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

Question

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

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

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

Answer 1

Я бы начал с однопараметрического класса типов с двумя связанными семействами типов для 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 буквально уравнения из вопроса.