3

我在 ghc 7.8.2 上玩 GADT 和明确的 forall。让我们看下面这个简单的例子：

{-# LANGUAGE GADTs, RankNTypes #-}

data T1 a where
   T1 :: (b -> a) -> b -> T1 a

data T2 a where
   T2 :: forall b. (b -> a) -> b -> T2 a

这里 ghc 失败了：

Test.hs:7:26: Not in scope: type variable ‘a’
Test.hs:7:35: Not in scope: type variable ‘a’

何时T2注释掉类型检查成功。但是T1和T2似乎是等价的。这是 ghc 中的错误还是 GADT 的某些限制？如果是后者，那么两者有什么区别？

4

2 回答 2

4

我最初假设a在T1构造函数中是在data T1 a声明时绑定的。但它实际上是在构造函数本身中隐式量化的。因此T2构造函数是错误的，因为它显式量化b而不量化a。

于 2014-05-24T21:25:14.957 回答
0

我正在努力解决类似的问题。根据 chi 的评论，我想出了这个解决方案：

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data T2 :: * -> * where
   T2 :: forall a b. (b -> a) -> b -> T2 a

与 相比，我更愿意b脱颖而出，但我想对于那些更喜欢它的人来说，这a仍然比隐含更好，其中包括我自己。forall

于 2016-01-28T13:37:18.567 回答