haskell – 使用PolyKinds的不明确类型

以下编译没有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')

zq的所有外观都是表示模运算模q的某种类型(种类*).用Nats代表这些模量很方便.如果我在类型族中添加PolyKinds和poly-kind模数:

{-# 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真的让这个含糊不清吗?歧义在哪里?还有关:When is -XAllowAmbiguousTypes appropriate?

如果我向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和模数(Zq 3)~3,Foo(Zq 3)3~(Zq 3)(我把工作从Foo类型族中剥离出来,所以把它想象成身份.)

我们暂时将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)))

所以问题是模数在其输出类型中是多态的,而Foo在其输入类型中是多态的.没有什么可以解决这种中间类型,所以它仍然是模棱两可的.修复它的一个选择是使用代理:

import Data.Proxy

...

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

现在你甚至可以再次删除Modulus和Foo的*注释,它仍然可以工作.

相关文章
相关标签/搜索