haskell - 将 Type.Equality 与 PolyKind 结合使用

Question

此编译代码是 this code 的最小化示例来自 this issue 的回答与语法2.0。我还使用源自 sameNat 的 sameModType 定义在数据.类型.平等中。

我一直在使用这个解决方案，没有出现任何问题，但我想让模数 q 成为一种多态，具体目标是制作 Proxy (nat::Nat) 为 nat::Nat(同时仍然能够使用 * 类型的模数)。

{-# LANGUAGE GADTs, 
             MultiParamTypeClasses, 
             FunctionalDependencies, 
             FlexibleContexts, 
             FlexibleInstances,
             TypeOperators, 
             ScopedTypeVariables,
             DataKinds,
             KindSignatures #-}

import Data.Tagged
import Data.Proxy
import Data.Type.Equality
import Data.Constraint
import Unsafe.Coerce
import GHC.TypeLits

newtype Zq q i = Zq i

data ZqType q
  where
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

class (Integral i) => Modulus a i | a -> i where
    value :: Tagged a i

instance (KnownNat q) => Modulus (Proxy (q :: Nat)) Int where 
    value = Tagged $ fromIntegral $ natVal (Proxy :: Proxy q)

sameModType :: (Modulus p i, Modulus q i) 
            => Proxy p -> Proxy q -> Maybe (p :~: q)
sameModType p q | (proxy value p) == (proxy value q) = 
                     Just $ unsafeCoerce Refl
                | otherwise = Nothing

typeEqSym :: ZqType p -> ZqType q -> Maybe (Dict (p ~ q))
typeEqSym (ZqType p) (ZqType q) = do
        Refl <- sameModType p q  -- LINE 39
        return Dict              -- LINE 40

但是当我将 -XPolyKinds 扩展添加到上面的代码中时，我收到几个编译错误:

Foo.hs:39:36:
    Could not deduce (k1 ~ k)
    ...
    Expected type: Proxy q0
      Actual type: Proxy q2
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the second argument of ‘sameFactoredType’, namely ‘q’
    In a stmt of a 'do' block: Refl <- sameFactoredType p q

Foo.hs:40:16:
    Could not deduce (k ~ k1)
    ...
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the first argument of ‘return’, namely ‘Dict’
    In a stmt of a 'do' block: return Dict
    In the expression:
      do { Refl <- sameFactoredType p q;
           return Dict }

Foo.hs:40:16:
    Could not deduce (q1 ~ q2)
    ...
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the first argument of ‘return’, namely ‘Dict’
    In a stmt of a 'do' block: return Dict
    In the expression:
      do { Refl <- sameFactoredType p q;
           return Dict }

我对类型相等的魔力了解不够，不知道如何解决这个问题。看来大多数有问题的类型在执行 GHC 所要求的约束方面都无可救药地超出了范围，但我以前在使用 PolyKinds 时从未遇到过此类问题。需要更改什么才能使代码使用 PolyKinds 进行编译？

Answer 1

我可以解释这个问题，但由于我不完全确定您想要做什么，所以我不确定如何最好地解决它。

问题出在 ZqType 的定义中:

data ZqType q
  where
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

ZqType 的类型参数称为 q，这有点误导。这是一个 GADT，类型参数与构造函数中出现的类型参数无关。我更喜欢给一个友善的签名。 ZqType 是什么样的？嗯，Zq q Int 是一种数据类型，因此它具有类型 *。您将 ZqType 应用于 Zq q Int，因此 ZqType 的类型为 * -> *(尽管PolyKind)。所以我们有

data ZqType :: * -> * where
  ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

接下来我们看看ZqType构造函数的类型是什么？没有多元种类，这就是你写下的内容:

ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

但是对于PolyKinds，q仅出现在种类多态位置，所以这变成:

ZqType :: forall (q :: k). (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

现在让我们看看如何在 sameModType 中使用它:

typeEqSym :: ZqType a -> ZqType b -> Maybe (Dict (a ~ b))
typeEqSym (ZqType p) (ZqType q) = do
  ...

我已重命名类型变量以避免混淆。因此，a 是一种 * 的未知类型，b 是 * 的另一种未知类型。您正在 GADT 上进行模式匹配。此时，GHC 得知 a 实际上是某种未知类型 k1 的未知 q1 的 Zq q1 Int 。此外，GHC 了解到，对于某种未知类型 k2 的未知 q2，b 实际上是 Zq q2 Int。特别是，我们不知道 k1 和 k2 是相同的，因为这没有强制执行。

然后，您继续调用 sameModType ，它期望两个代理属于同一类型，从而导致第一个此类错误。其余错误都是同一问题造成的。