[Haskell-cafe] Re: Developing Programs and Proofs Spontaneously using GADT

[apfelmus]

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