7

以下编译没有 PolyKinds：

{-# LANGUAGE TypeFamilies, GADTs #-}

type family Modulus zq

type family Foo zq q

data Bar :: (* -> *) where
    Bar :: (zq' ~ Foo zq (Modulus zq)) => Bar (zq -> zq')

的所有外观都是代表模算术 modzq的某种类型（种类） 。用它来表示这些模数会很方便。如果我在类型族中添加和多类模量：*qNatsPolyKinds

{-# LANGUAGE TypeFamilies, GADTs, PolyKinds #-}

type family Modulus zq :: k

type family Foo zq (q :: k)

data Bar :: (* -> *) where
    Bar :: (zq' ~ Foo zq (Modulus zq)) => Bar (zq -> zq')

GHC 7.8 抱怨：

Could not deduce (zq' ~ Foo zq (Modulus zq))
...
In the ambiguity check for:
  forall zq' zq. zq' ~ Foo zq (Modulus zq) => Bar (zq -> zq')
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘Bar’

添加PolyKinds 真的使这个模棱两可吗？歧义在哪里？还相关：-XAllowAmbiguousTypes 何时合适？

如果我向 GHC 扔骨头并将AllowAmbiguousTypes错误从 GADT 的声明移动到 GADT 的使用（没有添加扩展的建议）：

bar :: (zq' ~ Foo zq (Modulus zq))
  => Bar (zq -> zq')
bar = Bar

这让我觉得使用AllowAmbiguousTypes的是 GHC 红鲱鱼。

编辑

为了澄清，上面的类型可能被实例化如下：

newtype Zq q = Zq Int

然后zq ~ (Zq 3), q ~ 3, 和Modulus (Zq 3) ~ 3, Foo (Zq 3) 3 ~ (Zq 3)（我将工作从类型家族中剥离出来Foo，所以将其视为身份。）

4

1 回答 1

5

让我们暂时将zq参数限制为 kind ：*

type family Modulus (zq :: *) :: k

type family Foo (zq :: *) (q :: k)

然后你会得到一个稍微好一点的错误消息，可以通过说-fprint-explicit-kinds（假设 GHC 7.8）进一步改进：

Could not deduce ((~) * zq' (Foo k0 zq (Modulus k0 zq)))
from the context ((~) * zq' (Foo k zq (Modulus k zq)))

所以问题是Modulus它的输出类型Foo是多态的，并且它的输入类型是多态的。没有什么可以修复这种中间类型，所以它仍然模棱两可。修复它的一种选择是使用Proxy：

import Data.Proxy

...

data Bar :: (* -> *) where
    Bar :: (m ~ Modulus zq, zq' ~ Foo zq m) => Proxy m -> Bar (zq -> zq')

现在您甚至可以一次又一次地删除*注释Modulus，Foo它仍然可以工作。

于 2014-06-04T15:49:21.463 回答