1

理解我在问什么需要以下定义：

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 作为约束。我很迷茫，我不知道该去哪里。任何帮助或指导都是无价的。

4

1 回答 1

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是问题中的方程式。

于 2013-07-28T12:54:36.840 回答