定义幽灵类型 - 无法编译示例

Question

我正在尝试了解幻影类型。我正在阅读Ralf Hinze的《有趣的幻影类型》。他使用了一个我从未见过且无法编译的关键字with。当我尝试时，会出现=的解析错误。

data Type t = RInt                    with t = Int
            | RChar                   with t = Char
            | RList (Type a)          with t = [a ]
            | RPair (Type a) (Type b) with t = (a, b)

文章前面提到，"with"语句并非必需，可以通过设置a = t来实现，但是我无法在没有它们的情况下定义这种数据类型。以下错误提示：Not in scope: type variable 'a'

data Type t = RInt
            | RChar
            | RList (Type a)
            | RPair (Type a) (Type b)

我漏掉了什么？

- Sean Clark Hess

---

看起来使用GADTs很可能编写上述内容，但我仍然对Ralf的意图感兴趣。有没有特殊的关键字with？你能否在不使用GADTs的情况下表达这个意思？ - Sean Clark Hess

“如果我们有手段限制Term的类型参数为特定类型就好了。现在，正是上述‘温和’扩展允许我们这样做的时候了。通过这个扩展，我们声明Term数据类型如下…” 也许我理解错了，但我认为这是一个想象中的扩展，实际上并不存在（或者至少是我这么认为的），但是GADTs可以实现相同的效果;) - Random Dev

Answer 1

尽管有些丑陋，但以下内容将能够工作，且从实质上讲与该符号更为接近。这基本上是将GADT分解成类型等式（似乎没有它们自己的扩展名，因此您需要启用“GADTs”或“TypeFamilies”中的任一以使用它们）和存在性。

{-# LANGUAGE ExistentialQuantification, TypeFamilies #-}

data Type t = t ~ Int => RInt
            | t ~ Char => RChar
            | forall a. t ~ [a] => RList (Type a)
            | forall a b. t ~ (a, b) => RPair (Type a) (Type b)

- Ørjan Johansen

Answer 2

我的猜测是，论文中提出的“sans-with”定义是

data Type t = RInt
            | RChar
            | RList (Type t)
            | RPair (Type t) (Type t)

以上，参数t从未被使用。它实际上是虚假的。

这意味着，例如：

RInt :: Type a

对于任何类型a。相比之下，如果遵循with约束，则不可能为除t ~ Int之外的任何t创建RInt :: Type t。

with语法在GHC中不存在，但GADTs扮演基本相同的角色。

{-# LANGUAGE GADTs #-}
data Type t where
   RInt  :: t ~ Int   => Type t
   RChar :: t ~ Char  => Type t
   RList :: t ~ [a]   => Type a -> Type t
   RPair :: t ~ (a,b) => Type a -> Type b -> Type t

请注意，每个构造函数中的with被等式约束替换。实际上它们是相同的内容，只是表述方式不同。

更加简洁地，我们可以将以上内容改写为：

data Type t where
   RInt  :: Type Int
   RChar :: Type Char
   RList :: Type a -> Type [a]
   RPair :: Type a -> Type b -> Type (a,b)

约束已经“内联”在最终类型中。

- chi