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!
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
