理解我在问什么需要以下定义:
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 的第一个参数应该有 kind Param 但 Param 有 kind *,我不知道如何纠正这个问题。添加约束并使用变量时,我到了这里:
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 作为约束。我很迷茫,我不知道该去哪里。任何帮助或指导都是无价的。