haskell - 関数の入力と出力を導出するために再帰的な型レベル関数を開発しようとしています

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

もちろん、Haskell は Kind を制約として使用することを拒否しています。私はかなり迷っており、これでどこに行くべきかわかりません。ヘルプやガイダンスは非常に貴重です。