Corrispondenza modello Haskell su GADT con tipi di dati

Question

Ho scoperto che mi piace molto combinare GADT con Data Kinds, in quanto mi dà ulteriore sicurezza del tipo rispetto a prima (per la maggior parte degli usi, quasi come Coq, Agda et al.). Purtroppo, la corrispondenza dei modelli fallisce con il più semplice degli esempi e non riesco a pensare a nessun modo di scrivere le mie funzioni ad eccezione delle classi di tipi.

Ecco un esempio per spiegare il mio dolore:

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 

Abbiamo 2 classi di tipo (una per il teorema, una per un'operazione di utilità) e 5 casi - solo per un teorema banale. Idealmente, Haskell potrebbe guardare questa funzione:

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

e il tipo di controllare ogni clausola di per sé, e per-call decidere quali casi sono possibili (e quindi la pena cercare di abbinare) e che non sono, così quando si chiama trans Le_base Le_base Haskell noterà che solo il primo caso consente alle tre variabili di essere uguali e tentare solo la corrispondenza sulla prima clausola.

Answer 1

Non vedo come la definizione del modello di corrispondenza di trans funzionerebbe in Agda o Coq.

Se si scrive il seguente, invece, funziona:

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

Naturalmente, si potrebbe anche definire in modo più diretto:

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)