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 == Boolや:kind! Int == Intや:kind! Z == Zのようなことができます:kind! (I Z (S Z)) == (I (S Z) (S (S Z)))。

type +ただし、アドホックなポリモーフィックを作成したいと考えています。私が与えたインスタンスに制約されるように。ここでの 2 つのインスタンスは、 kind のNatK型と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に制約する必要がある拡張機能と関係がありますか?:+Add

4

2 に答える 2

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 に答える