haskell - 使用 PolyKinds 和类型系列时出现类型歧义

Question

我有两个类型系列，其中一个将一种类型映射到另一种不同种类和多态函数的类型:

{-# 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

Answer 1

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] ，但是G是一个非单射类型族，因此无法得知它的任何一个参数是什么 - k2和F Char :: k2 -应该。因此，x的定义是有错误的； k2是不明确的，不可能推断出它的实例化。

但是，您可以非常清楚地看到没有使用 f 永远能够推断 k2 。推理是k2仅出现在 f 类型中在非单射类型系列应用程序下方(另一个“坏位置”是 => 的 LHS)。它永远不会出现在可以推断的位置。因此，没有像 TypeApplications 这样的扩展名, f 无用，并且永远不能在不引发此错误的情况下提及。 GHC 会检测到这一点并在定义而不是用法上引发错误。您看到的错误消息与您尝试以下操作时收到的错误消息大致相同:

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

这会产生相同的类型不匹配，因为没有理由 k20的f0必须匹配k2的f1 .

您可以消除 f 定义中的错误通过启用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 这样的东西，它就真的失去了作用。)