5

我有两个类型族，其中一个将一种类型映射到另一种类型和多态函数的另一种类型：

{-# LANGUAGE PolyKinds, TypeFamilies, FlexibleContexts, ScopedTypeVariables #-} 

type family F (a :: k1) :: k2
type family G (a :: k2) :: *

f :: forall k1 k2 (a :: k1) (p :: k1 -> *) . p (a :: k1) -> G (F (a :: k1) :: k2)
f = undefined

此代码不使用以下错误消息进行类型检查：

• Couldn't match type ‘G k20 (F k20 k1 a)’ with ‘G k2 (F k2 k1 a)’
  Expected type: p a -> G k2 (F k2 k1 a)
    Actual type: p a -> G k20 (F k20 k1 a)
  NB: ‘G’ is a non-injective type family

但我不明白歧义来自哪里以及如何指定缺失的种类？

当我只使用一种类型系列时，它可以工作：

g :: forall k1 k2 (a :: k1) (p :: k1 -> *) (q :: k2 -> *). p (a :: k1) -> q (F (a :: k1) :: k2)
g = undefined
4

2 回答 2

6 
f :: forall k1 k2 (a :: k1) (p :: k1 -> *). p a -> G (F a :: k2)

让我试着说：

x :: [String]
x = f (Just 'a')

f这会用k1 ~ Type,a ~ Char和实例化p ~ Maybe

f :: forall k2. Maybe Char -> G (F Char :: k2)

怎么办？好吧，我还需要G (F Char :: k2) ~ [String], butG是一个非内射类型族，所以不知道它的参数——<code>k2 和——F Char :: k2应该是什么。因此， 的定义x是错误的；k2是模棱两可的，不可能为其推断实例化。

但是，您可以非常清楚地看到，将永远无法推断出. 原因是它只出现在非内射类型族应用程序下面的类型中（另一个“坏位置”是 a 的 LHS ）。它永远不会出现在可以推断的位置。因此，没有像,这样的扩展是没有用的，并且永远不能在不引发此错误的情况下提及。GHC 会检测到这一点，并在定义而不是用法上引发错误。您看到的错误消息与您尝试时遇到的错误大致相同：fk2k2f=>TypeApplicationsf

f0 :: forall k10 k20 (a :: k10) (p0 :: k10 -> *). p0 a0 -> G (F a0 :: k20)
f0 = f

这会产生相同的类型不匹配，因为没有理由k20off0必须匹配k2of f1。

您可以f通过enable 来消除定义中的错误AllowAmbiguousTypes，这会禁用对所有定义的无用检查。但是，仅此而已，这只会将错误推向f. 为了实际调用f，您应该启用TypeApplications：

f0 :: forall k10 k20 (a :: k10) (p0 :: k10 -> *). p0 a0 -> G (F a0 :: k20)
f0 = f @k10 @k20 @a0 @p0

的替代方法TypeApplications类似于Data.Proxy.Proxy，但这已经过时了，除非在更高级别的上下文中。（即便如此，一旦我们有了type-lambdas之类的东西，它真的会失去作用。）

于 2019-01-13T21:36:39.447 回答
2

歧义检查最初旨在拒绝无法调用的函数，因为类型参数和约束无法从显式函数参数中推断出来。

然而，从 GHC 8.6.x 开始，没有这样的函数，因为一切都可以通过TypeApplications. 我建议只启用AllowAmbiguousTypesand TypeApplications。GHC 关于模棱两可类型的警告本身并不能提供很多信息，因为它拒绝了类型应用程序的许多有效用例。

于 2019-01-13T21:43:17.833 回答