Haskell Pattern Matching auf GADTs mit Data Kinds

Question

Ich habe festgestellt, dass ich GADTs mit Data Kinds kombiniere, da es mir mehr Sicherheit gibt (für die meisten Anwendungen fast so gut wie Coq, Agda et al.). Leider schlägt die Mustererkennung bei den einfachsten Beispielen fehl, und ich konnte mir keine andere Möglichkeit vorstellen, meine Funktionen außer für Typklassen zu schreiben.

Hier ist ein Beispiel meiner Trauer zu erklären:

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 

Wir haben 2 Typklassen (ein für den Satz, ein für einen Utility-Betrieb) und 5 Fälle - nur für einen trivialen Satz. Idealerweise könnte Haskell in dieser Funktion aussehen:

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

und jede Klausel auf seinem eigenen Art-Check-in und pro-Anruf entscheiden, welche Fälle möglich ist (also ein Versuch wert zu entsprechen) und welche nicht, so beim Aufruf trans Le_base Le_base Haskell wird bemerken, dass nur der erste Fall zulässt, dass die drei Variablen identisch sind, und versuchen nur, die Übereinstimmung mit der ersten Klausel zu finden.

Answer 1

Ich sehe nicht, wie Ihre Pattern-Matching-Definition von trans in Agda oder Coq funktionieren würde.

Wenn Sie die folgenden stattdessen schreiben, es funktioniert:

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

Natürlich könnten Sie auch direkt definieren:

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)