Shin-Cheng Mu wrote:
I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language.
In the exercise below, I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna's introduction to Epigram [1]: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one. The property I am going to show is merely that the length of the input list is preserved.
Cool! :)
Given that dependent types and GADTs are such popular topics, I believe the same must have been done before, and there may be better ways to do it. If so, please give me some comments or references. Any comments are welcomed.
{-# OPTIONS_GHC -fglasgow-exts #-}
To begin with, we define the usual type-level representation of natural numbers and lists indexed by their lengths.
data Z = Z deriving Show data S a = S a deriving Show
data List a n where Nil :: List a Z Cons :: a -> List a n -> List a (S n)
1. Append
To warm up, let us see the familiar "append" example. Unfortunately, unlike Omega, Haskell does not provide type functions. I am not sure which is the best way to emulate type functions. One possibility is to introduce the following GADT:
data Plus m n k where --- m + n = k PlusZ :: Plus Z n n PlusS :: Plus m n k -> Plus (S m) n (S k)
such that Plus m n k represents a proof that m + n = k.
Wouldn't type families (~ associated type synonyms) do exactly that once they become available? type family Plus :: * -> * -> * type instance Plus Z n = n type instance Plus (S m) n = S (Plus m n) append :: (Plus m n ~ k) => List a m -> List a n -> List a k append Nil ys = ys append (Cons x xs) ys = Cons x (append xs ys) But I'd guess that there are some constraints on the type family instance declarations to keep things decidable. Viewed with the dictionary translation for type classes in mind, this is probably exactly the alternative type of append you propose: append :: Plus m n k -> List a m -> List a n -> List a k
However, this does not type check. Assume that t has size n1, and u has size n. The DepSum returned by merge consists of a list of size i, and a proof p of type Plus m n i, for some i. The proof p1, on the other hand, is of type P m n k for some k. Haskell does not know that Plus m n is actually a function and cannot conclude that i=k.
To explicitly state the equality, we assume that there is a function plusFn which, given a proof of m + n = i and a proof of m + n = k, yields a function converting an i in any context to a k. That is:
plusFn :: Plus m n i -> Plus m n k -> (forall f . f i -> f k)
How do I define plusFn? I would like to employ the techniques related to equality types [3,4,5], but currently I have not yet figured out how. I've merely produced a version of plusFn specialised to List a:
plusFn :: Plus m n h -> Plus m n k -> List a h -> List a k plusFn PlusZ PlusZ xs = xs plusFn (PlusS p1) (PlusS p2) (Cons x xs) = Cons x (plusFn p1 p2 xs)
Needless to say this is not satisfactory.
I remember that the newtype Equal a b = Proof (forall f . f a -> f b) type equality has been used to define/implement GADTs Ralf Hinze. Fun with phantom types. http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf so a general plusFn ought to be possible. I think that the following induction should work (untested!): equalZ :: Equal Z Z equalS :: Equal m n -> Equal (S n) (S m) plusFn :: Plus m n i -> Plus m n k -> Equal i k plusFn PlusZ PlusZ = equalZ plusFn (PlusS x) (PlusS y) = equalS (plusFn x y) with the "trivial" equality proofs for natural numbers equalZ = Proof id newtype Succ f a = InSucc { outSucc :: f (S a) } equalS (Proof eq) = Proof (outSucc . eq . InSucc) The newtype is just for making the type checker recognize that f (S a) is indeed of the form g a for some type constructor g . Regards, apfelmus