7

我正在研究 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 == Boolor:kind! Int == Int或:kind! Z == Zand的事情:kind! (I Z (S Z)) == (I (S Z) (S (S Z)))。

但是我想使type +临时多态。所以它仅限于我给它的实例。这里的 2 个实例是 kindNatK类型和 kind 类型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扩展有关，我需要将:+or限制Add为某种“类”？

4

2 回答 2

8

最简单的解决方案是使用开放类型族进行临时重载，使用封闭类型族进行实现：

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
于 2016-03-18T09:01:01.267 回答
1

（这应该是评论，但我需要更多空间）

我尝试了类似的东西

class GoodK (Proxy k) => NumK (a :: k) (b :: k) where ...

但我失败了。我不知道你的要求是否可以实现。

我得到的最好的近似值是进行Add Bool Bool种类检查，但会产生一个无法解决的约束，所以如果我们使用它，无论如何我们都会得到一个错误。也许这足以满足您的目的（？）。

class Fail a where

instance Fail a => NumK (a :: *) (b :: *) where
    type Add a b = ()
于 2016-03-18T09:00:02.543 回答