将Type.Equality与PolyKinds一起使用

Question

这编译代码是一个最小化的例子的代码从一个答案,这个问题与句法2.0.我也在Data.Type.Equality中使用sameModType派生的定义sameNat.

我一直在使用这个解决方案没有问题,但我想使模数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是* -> *(尽管PolyKindS).所以我们有

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实际上Zq q1 Int是某种未知q1的未知类型k1.此外,GHC得知b实际上是Zq q2 Int由于一些未知的q2一些未知的那种k2.特别是,我们在这里并不知道k1并且k2是相同的,因为这是无处可执行的.

然后你继续调用sameModType哪个代理需要相同类型,导致你的第一个错误.剩下的错误都是同一问题的结果.

Answer 2

我不知道这是否是您正在寻找的，但您可以简单地公开底层参数的类型以供以后使用：

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

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

instance Modulus Int Int where 
instance Modulus (n :: Nat) Int where 

KProxy应该在Data.Proxy，但也只是data KProxy (x :: *) = KProxy。

人为的例子：

>let x = ZqType (Proxy :: Proxy (10 :: Nat))
>let y = ZqType (Proxy :: Proxy Int)
>typeEqSym x y
<interactive>:25:13:
    Couldn't match kind `*' with `Nat'
    Expected type: ZqType (Zq Int Int) 'KProxy
      Actual type: ZqType (Zq Int Int) 'KProxy
    In the second argument of `typeEqSym', namely `y'
    In the expression: typeEqSym x y