[Haskell-cafe] Safe lists with GADT's

[Stefan O'Rear]

On Mon, Feb 26, 2007 at 04:35:06PM +0100, Pepe Iborra wrote:
> I am really curious about this style of programming, and find myself  
> playing with it from time to time.
> The example so far is very nice, but the funniest part is missing.  
> That is, defining appendL.
> 
> > appendL :: List a t1 -> List a t2 -> List a t3
> 
> This says that the append of a list of length t1 and a list of length  
> t2 is a list of whatever length t3 we want. Obviously this is not  
> true and will not typecheck.
> After some healthy days of reading papers and theses, I've found at  
> least three ways of defining it.
> 
> First, via existentials:
> > appendL1 :: List a t1 -> List a t2 -> exists t3. List a t3
> 
> Second, attaching a proof. Question: what would be the advantage of  
> the proof here?
> > data Add a b c where Base :: Add NilT a a ; Step :: Add a b c ->  
> Add (ConsT a) b (ConsT c)
> > appendL2 :: List a t1 -> List a t2 -> exists t3. (Add t1 t2 t3,  
> List a t3)
> 
> Third, via Type Classes.
> \begin{code}
> class AddList a b c | a b -> c
>         where append :: List x a -> List x b -> List x c
> instance AddList NilT b b
>         where append Nil x = x
> instance AddList a b c => AddList (ConsT a) b (ConsT c)
>         where append (Cons x l) l' = Cons x (append l l')
> \end{code}
> 
> 
> Given the three methods, I wouldn't know which one should be  
> preferred, and why.
> In the first one you pay the burden of programming with existentials.
> The second one in addition to that is the least efficient, as  
> building the proof surely has a cost. Since we are building it, isn't  
> there a way to use it to remove the existential?
> Finally, with the third one your compiler will produce error messages  
> that will make you swear, apart from possible efficiency losses too.

Personally I like the GADT approach best since it is very flexible and
convienient.  I have never used a purpose-build computer proof system,
but (modulo _|_) it took me less than 10 minutes to answer LoganCapaldo
(on #haskell)'s challenge to proof that + was commutative ( http://hpaste.org/522 ).

Now, efficiency concerns.  GHC haskell already uses higher-than-value-level
proofs to implement newtypes/GADTs/ATs; efficiency concerns are addressed
in a strikingly adhoc way, by promoting equality to the KIND level, allowing
type erasure to remove the overhead of checking.  Chakravarty, Peyton Jones,
we'd really like a general kind-level proof system!