haskell - 如何约束类型族中的种类

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