如何约束类型族中的类型

Question

在我最近的一个问题中，我发现answer 使用了一个类型类。注意HasNProxyK k 中，k 是第二个NProxyK 参数的类型。

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}

import GHC.TypeLits hiding ( (*) )
import Data.Kind

class HasNProxyK j where
  data NProxyK (n :: Nat) (a::j) :: k
instance HasNProxyK Type where
  data NProxyK n a = NProxyK0
instance HasNProxyK k => HasNProxyK (j -> k) where
  data NProxyK n f = NProxyKSuc -- or NProxyKS (ProxyK n (f a))

type family ToNProxyK (n :: Nat) (a :: k) :: k where
  ToNProxyK n (a :: Type) = NProxyK n a
  ToNProxyK n (a :: j -> k) = NProxyK n a

我至少在一个方面对上述内容不满意。我本来想用constraint in its kind 声明类型族，例如：

type family ToNProxyK (n :: Nat) (a :: HasNProxyK k => k) :: k where
   ToNProxyK n (a::Type) = Type
   ToNProxyK n (a :: j -> k) = NProxyK n a

我的意图是限制a 属于HasNProxyK。为了使用类型族，我必须知道类实例是满意的——希望在编译时捕获像ToNProxyK 3 True 这样的声明。但是，当我尝试上面的 ghc 时告诉我：

src/Traversal.hs:359:15: error:
    • Expected kind ‘HasNProxyK k0 => k0’,
        but ‘(a :: Type)’ has kind ‘*’
    • In the second argument of ‘ToNProxyK’, namely ‘(a :: Type)’
      In the type family declaration for ‘ToNProxyK’
    |
359 |   ToNProxyK n (a :: Type) = NProxyK n a
    |               ^^^^^^^^^^^

我从中得到的是，我实际上并没有声明我认为我在声明的内容。我已经指定了一种新的种类，而不仅仅是限制了 被接受。我也尝试在成员类型 (HasNProxyK Type => Type) 中包含约束，但这只会导致其他问题。

那么，我实际上在我受约束的善良家庭中声明了什么？有没有办法在这个类型族中限制 k 以禁止 ToNProxyK n True 之类的类型？

Answer 1

据我所知，我找不到实现约束封闭类型族的完美方法，这就是您想要的。

但是，对于您的具体情况，使用在类型类中声明的类型族可能就足够了，它允许您根据需要约束 k。

class HasNProxyK k => C k (n :: Nat) (a :: k) where
    type ToNProxyK k n a :: k

instance C Type n a where
    type ToNProxyK Type n a = NProxyK n a

instance HasNProxyK k => C (j -> k) n a where
    type ToNProxyK (j -> k) n a = NProxyK n a

通过这样做，我们失去了对 封闭 类型族的“自上而下”处理。在您的情况下，Type 和 j -> k 之间没有重叠，所以这应该不是问题。

---

更简单的变体：

class HasNProxyK k => C k where
    type ToNProxyK k (n :: Nat) (a :: k) :: k

instance C Type where
    type ToNProxyK Type n a = NProxyK n a

instance HasNProxyK k => C (j -> k) where
    type ToNProxyK (j -> k) n a = NProxyK n a