如何在Haskell中创建"kind类",或者使用类型族在类型级创建ad-hoc多态

Question

我正在研究Haskell的类型族特征,以及类型级计算.看起来很容易使用以下方法获得类型级别的参数多态性PolyKinds:

{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators, UndecidableInstances, PolyKinds, MultiParamTypeClasses, FlexibleInstances #-}

data NatK = Z | S NatK
data IntK = I NatK NatK

infix 6 +
type family (x :: NatK) + (y :: NatK) :: NatK where
    Z     + y = y
    (S x) + y = S (x + y)

-- here's a parametrically polymorphic (==) at the type-level
-- it also deals specifically with the I type of kind IntK
infix 4 ==
type family (a :: k) == (b :: k) :: Bool where
    (I a1 a2) == (I b1 b2) = (a1 + b2) == (a2 + b1)
    a == a = True
    a == b = False

我可以做像:kind! Bool == Bool或:kind! Int == Int或:kind! Z == Z和:kind! (I Z (S Z)) == (I (S Z) (S (S Z))).

但是我想制作type +ad-hoc多态.因此它受限于我给它的实例.这里的2个实例将是种类NatK和类型IntK.

我首先尝试使其参数化多态:

infix 6 :+
type family (x :: k) :+ (y :: k) :: k where
    Z         :+ y = y
    (S x)     :+ y = S (x :+ y)
    (I x1 x2) :+ (I y1 y2) = I (x1 :+ y1) (x2 :+ y2)

这正如我所能做的那样有效:kind! (I (S Z) Z) :+ (I (S Z) Z).

不过我也可以:kind! Bool :+ Bool.这没有任何意义,但它允许它作为一个简单的类型构造函数.我想创建一个不允许这种错误类型的类型系列.

此时我迷失了.我尝试用type参数输入类.但那没用.

class NumK (a :: k) (b :: k) where
    type Add a b :: k

instance NumK (Z :: NatK) (b :: NatK) where
    type Add Z b = b

instance NumK (S a :: NatK) (b :: NatK) where
    type Add (S a) b = S (Add a b)

instance NumK (I a1 a2 :: IntK) (I b1 b2 :: IntK) where
    type Add (I a1 a2) (I b1 b2) = I (Add a1 b1) (Add a2 b2)

它仍然允许:kind! Add Bool Bool.

这是否与ConstraintKinds扩展有关,我需要约束:+或者Add某些"善类"？

Answer 1

最简单的解决方案是使用开放类型系列进行ad-hoc重载和封闭类型系列的实现:

data NatK = Z | S NatK
data IntK = I NatK NatK

type family Add (x :: k) (y :: k) :: k

type family AddNatK (a :: NatK) (b :: NatK) where
  AddNatK Z b = b
  AddNatK (S a) b = S (AddNatK a b)

type family AddIntK (a :: IntK) (b :: IntK) where
  AddIntK (I a b) (I a' b') = I (AddNatK a a') (AddNatK b b')

type instance Add (a :: NatK) (b :: NatK) = AddNatK a b
type instance Add (a :: IntK) (b :: IntK) = AddIntK a b

如果我们想要将多个类型级和术语级方法组合在一起,我们可以使用KProxyfrom 来编写类类Data.Proxy:

class NumKind (kproxy :: KProxy k) where
  type Add (a :: k) (b :: k) :: k
  -- possibly other methods on type or term level

instance NumKind ('KProxy :: KProxy NatK) where
  type Add a b = AddNatK a b

instance NumKind ('KProxy :: KProxy IntK) where
  type Add a b = AddIntK a b

当然,关联类型与开放类型系列相同,因此我们也可以使用开放类型系列,并为术语级方法使用单独的类.但我认为将所有重载的名称放在同一个类中通常更清晰.

从GHC 8.0开始,KProxy变得不必要,因为种类和类型将以完全相同的方式处理:

{-# LANGUAGE TypeInType #-}

import Data.Kind (Type)

class NumKind (k :: Type) where
  type Add (a :: k) (b :: k) :: k

instance NumKind NatK where
  type Add a b = AddNatK a b

instance NumKind IntK where
  type Add a b = AddIntK a b