Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Haskell pattern matching on GADTs with Data Kinds

I have found that I really like combining GADTs with Data Kinds, as it gives me further type safety than before (for most uses, almost as good as Coq, Agda et al.). Sadly, pattern matching fails on the simplest of examples, and I could think of no way to write my functions except for type classes.

Here's an example to explain my sorrow:

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

We have 2 type classes (one for the theorem, one for a utility operation) and 5 instances - just for a trivial theorem. Ideally, Haskell could look at this function:

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

And type-check each clause on its own, and per-call decide which cases are possible (thus worth trying to match) and which are not, so when calling trans Le_base Le_base Haskell will notice that only the first case allows for the three variables to be the same, and only attempt matching on the first clause.

like image 235
Ramon Snir Avatar asked Aug 22 '12 06:08

Ramon Snir


People also ask

Does Haskell have pattern matching?

Overview. We use pattern matching in Haskell to simplify our codes by identifying specific types of expression. We can also use if-else as an alternative to pattern matching. Pattern matching can also be seen as a kind of dynamic polymorphism where, based on the parameter list, different methods can be executed.

How does pattern matching work in Haskell?

Pattern matching consists of specifying patterns to which some data should conform and then checking to see if it does and deconstructing the data according to those patterns. When defining functions, you can define separate function bodies for different patterns.


1 Answers

I don't see how your pattern-matching definition of trans would work in Agda or Coq.

If you write the following instead, it works:

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

Of course, you could also more directly define:

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)
like image 115
kosmikus Avatar answered Oct 02 '22 14:10

kosmikus