GADTとデータ型のHaskellパターンマッチング

Question

GADTとデータ型を組み合わせるのが本当に好きです。以前よりも型の安全性が向上しています（ほとんどの場合、AgqなどのCoqとほとんど同じです）。悲しいことに、最も単純な例ではパターンマッチングは失敗し、型クラス以外の関数を書く方法はないと思います。

は、ここに私の悲しみを説明するための例です：

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つのインスタンスを持っている - ちょうど些細な定理のために。呼び出すとき

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

そして独自に各句をタイプチェック、および（一致しようとしているので、価値が）可能である場合を決めるごとの呼び出し、どのように、ではありません。理想的には、Haskellはこの機能で見ることができますtrans Le_base Le_base Haskellは、最初のケースだけが3つの変数が同じであることを許し、最初の句で一致を試みることに気づくでしょう。

Answer 1

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)