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!