3

我一直在尝试使用 rank-2 类型在 PureScript 中对 GADT 进行编码，如此处所述的Haskell

我的代码如下所示：

data Z
data S n

data List a n 
  = Nil (Z -> n)
  | Cons forall m. a (List a m) (S m -> n)

fw :: forall f a. (Functor f) => (forall b . (a -> b) -> f b) -> f a
fw f = f id

bw :: forall f a. (Functor f) => f a -> (forall b . (a -> b) -> f b)
bw x f = map f x

nil :: forall a. List a Z
nil = fw Nil

cons :: forall a n. a -> List a (S n)
cons a as = fw (Cons a as)


instance listFunctor :: Functor (List a) where
    map f (Nil k) = Nil (f <<< k)
    map f (Cons x xs k) = Cons x xs (f <<< k)

编译器抱怨Wrong number of arguments to constructor Main.Cons，指的是 Functor 实例中的 LHS 模式匹配。

这里出了什么问题？

问候，

迈克尔

4

1 回答 1

5

在 Haskell 中用于存在类型的语法在 PureScript 中不存在。您所写的Cons是一个具有单个普遍量化参数的数据构造函数。

您可能想尝试使用purescript-exists来编码存在类型。

另一种选择是使用 GADT 的最终无标签编码：

class Listy l where
  nil :: forall a. l Z a
  cons :: forall a n. a -> l n a -> l (S n) a

您可以为任何有效Listy实例编写术语：

myList :: forall l. (Listy l) => l (S (S Z)) Int
myList = cons 1 (cons 2 nil)

并通过编写实例来解释它们

newtype Length n a = Length Int

instance lengthListy :: Listy Length where
  nil = Length 0
  cons _ (Length n) = Length (n + 1)

newtype AsList n a = AsList (List a)

instance asListListy :: Listy AsList where
  nil = AsList Nil
  cons x (AsList xs) = AsList (Cons x xs)
于 2015-07-23T18:27:56.207 回答