15

GADTとDataKindsを組み合わせるのが本当に好きであることがわかりました。これにより、以前よりも型の安全性が向上します（ほとんどの用途で、Coq、Agdaなどとほぼ同じです）。悲しいことに、パターンマッチングは最も単純な例では失敗し、型クラス以外の関数を作成する方法は考えられませんでした。

これが私の悲しみを説明する例です：

data Nat = Z | S Nat deriving Eq

data Le :: Nat -> Nat -> * where
    Le_base :: Le a a
    Le_S :: Le a b -> Le a (S b)

class ReformOp n m where
    reform :: Le (S n) (S m) -> Le n m

instance ReformOp a a where
    reform Le_base = Le_base

instance ReformOp a b => ReformOp a (S b) where
    reform (Le_S p) = Le_S $ reform p

class TransThm a b c where
    trans :: Le a b -> Le b c -> Le a c

instance TransThm a a a where
    trans = const

instance TransThm a a b => TransThm a a (S b) where
    trans Le_base (Le_S p) = Le_S $ trans Le_base p

instance (TransThm a b c, ReformOp b c) => TransThm a (S b) (S c) where
    trans (Le_S p) q = Le_S $ trans p $ reform q

2つの型クラス（1つは定理用、もう1つはユーティリティ操作用）と5つのインスタンスがあります-些細な定理用です。理想的には、Haskellはこの関数を見ることができます：

-- not working, I understand why
trans :: Le a b -> Le b c -> Le a c
trans Le_base Le_base = Le_base
trans Le_base (Le_S p) = Le_S $ trans Le_base p
trans (Le_S p) q = Le_S $ trans p $ reform q

そして、各句を独自にタイプチェックし、呼び出しごとに、どのケースが可能で（したがって、一致させる価値があります）、どれが不可能であるかを決定します。したがって、trans Le_base Le_baseHaskellを呼び出すと、最初のケースのみが3つの変数を許可することに気付きます。同じで、最初の句でのみ一致を試みます。

4

1 に答える 1

14

transのパターンマッチング定義がAgda または Coq でどのように機能するかわかりません。

代わりに次のように書くと、うまくいきます。

reform :: Le (S n) (S m) -> Le n m
reform Le_base         = Le_base
reform (Le_S Le_base)  = Le_S Le_base
reform (Le_S (Le_S p)) = Le_S (reform (Le_S p))

trans :: Le a b -> Le b c -> Le a c
trans Le_base  q        = q
trans (Le_S p) Le_base  = Le_S p
trans (Le_S p) (Le_S q) = Le_S (trans p (reform (Le_S q)))

もちろん、より直接的に定義することもできます:

trans :: Le a b -> Le b c -> Le a c
trans p Le_base  = p
trans p (Le_S q) = Le_S (trans p q)
于 2012-08-22T07:23:45.677 に答える