Haskellで "kindクラス"を作成する方法、またはタイプファミリを使用して型レベルでアドホック多型を作成する

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 +アドホック多型を作りたいと思います。それは私がそれを与えるインスタンスに制約されるように。ここの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でも可能です。

これは、:+またはAddを「kind class」に制限する必要があるConstraintKinds拡張と関係しますか？

Answer 1

最も簡単な解決策は、実装のためのアドホックな過負荷と密閉型の家族のための開放型ファミリを使用することです：私たちは一緒にグループ化された複数の種類のレベルおよび用語レベルのメソッドを使用する場合は

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 

我々はData.ProxyからKProxyを使用して使用した種類のクラスを記述することができます。

もちろん

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 

、関連するタイプは、オープンタイプのFAMILIEと同じですしたがって、用語レベルのメソッドに別のクラスを持つオープン型のファミリを使用することもできました。しかし、私はそれが一般的に同じクラスのすべてのオーバーロードされた名前を持っているクリーナーだと思う。

{-# 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 

Answer 2

（これはコメントする必要がありますが、私はより多くのスペースを必要とする）

私は

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 =()