Попытка разработать рекурсивную функцию уровня типа для получения ввода и вывода функции

Следующие определения необходимы, чтобы понять, о чем я спрашиваю:

data Param = PA | PB | PC

data R p a where
  A :: S a -> R PA (S a)
  B :: S a -> R PB (S a)

data S a where
  Prim :: a -> S a
  HO   :: R pa a -> R pb b -> S ((R pa a) -> (R pb b))
  Pair :: R pa a -> R pb b -> S ((R pa a), (R pb b))

data Box r a = Box r a

Я хотел бы написать функцию, используя эти определения, которая работает следующим образом:

trans :: t -> TransIn t -> TransOut t

куда

TransIn (R 'PA (S a)) = a
TransIn (R 'PB (S a)) = a
TransIn (R 'PA (S (r1, r2))) = (TransIn r1, TransIn r2)
TransIn (R 'PA (S (r1, r2))) = (TransIn r1, TransIn r2)
TransIn (R 'PA (S (r1 -> r2))) = Error
TransIn (R 'PB (S (r1 -> r2))) = TransOut r1 -> TransIn r2

и

TransOut (R 'PA (S a)) = Box (R 'PA (S a)) a
TransOut (R 'PB (S a)) = Box (R 'PB (S a)) a
TransOut (R 'PA (S (r1, r2))) = (TransOut r1, TransOut r2)
TransOut (R 'PA (S ((R p (S a)), R p (S b))))) = (Box (R p (S a)) a, Box (R p (S b)) b)
TransOut (R 'PA (S (r1 -> r2))) = Error
TransOut (R 'PB (S (r1 -> r2))) = TransIn r1 -> TransOut r2

Основная идея состоит в том, чтобы принимать различные формы ввода и создавать различные формы вывода на основе конструктора, используемого для S, и параметра, выбранного при построении R. Я пытался сделать это, используя классы с типами данных, но я получаю типа ошибки несоответствия. Мне было интересно, есть ли интуитивно понятный, чистый способ кодировать такие вещи.

Текущая попытка у меня выглядит следующим образом:

class Transform t a where
  data TransIn t a:: *
  data TransOut t a:: *
  trans :: t -> TransIn t a -> TransOut t a

instance Transform (R Param (S a)) a where
  data TransIn (A (S a)) a :: a
  data TransOut (A (S a)) a :: Box (R Param (S a)) a
  trans t a = Box t a

instance Transform (R Param (S (a -> b))) a where
  data TransIn (A (S (a -> b))) (a -> b) :: TransIn a -> TransIn b
  data TransOut (A (S (a -> b))) (a -> b) :: TransOut a -> TransOut b
  trans _ _ = undefined

Этот подход жалуется, что первый аргумент R должен иметь вид Param, но Param имеет вид *, и я не уверен, как это исправить. При добавлении ограничения и использовании переменной я получил вот это:

instance (p :: Param) => Transform (R p (S a)) a where
  data TransIn (R p (S a))) a :: a
  data TransOut (R p (S a)) a :: Box (R p (S a)) a
  trans t a = Box t a

Конечно, Haskell не позволил мне использовать вид в качестве ограничения. Я довольно потерян, и я не уверен, куда идти с этим. Любая помощь или руководство были бы неоценимы.


typeclass haskell gadt data-kinds
person kaosjester    schedule 28.07.2013    source источник
comment
Я думаю, что это опечатка: вторая копия строки TransIn (R 'PA (S (r1, r2))) = (TransIn r1, TransIn r2) должна быть TransIn (R 'PB ...) = .... И то же самое для TransOut.   -  person Toxaris    schedule 28.07.2013

Ответы (1)


arrow_upward
1
arrow_downward

Я бы начал с класса типов с одним параметром и двумя связанными семействами типов для TransIn и TransOut.

class Transform t where
  type TransIn t
  type TransOut t
  trans :: t -> TransIn t -> TransOut t

Теперь вам нужно шесть экземпляров для шести уравнений для TypeIn и TypeOut. Вот первый.

instance Transform (R PA (S a)) where
  type TransIn (R PA (S a)) = a
  type TransOut (R PA (S a)) = Box (R PA (S a)) a
  trans t a = error "implement me!"

Обратите внимание, что определения для TransIn и TransOut буквально являются уравнениями из вопроса.

person Toxaris    schedule 28.07.2013