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.
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.
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.
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)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With