[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs

[Conor McBride]

Keean Schupke wrote:
> Conor,
> 
>    I thought you might like this... It shows how to do this without 
> phantom types! (we just use scoped type variables to help the 
> typechecker sort things out)... What do you think? Does this overcome 
> all the problems with Olegs approach? (the only slight problem I have 
> found is that you must give the parameters explicitly for definitions 
> like test3)

Yeah, that's nice. Scoped type variables are really handy for this sort
of thing. You've got rid of the annotation on application (hey, what are
typecheckers for?) but it's not so easy to lose it on the lambda: you
need that for the fundep. To have a good story here, we need to show
either how to get rid of the fundep or how to ensure we always have one.

Meanwhile, Oleg wrote:
 > class OpenExpression t env r | t env -> r where
 >    efold :: t -> env
 > 	     -> (forall r. r -> c r) -- Constant
 > 	     -> (forall r. r -> c r) -- Symbol
 > 	     -> (forall a r. (a -> c r) -> c (a->r))  -- Lambda
 > 	     -> (forall a r. c (a->r) -> c a -> c r) -- Application
 >	     -> c r

Funny you should say that. That's rather close to the traditional way
inductive datatype families have been presented for lord knows how long:
a bunch of constructors and an elimination operator, aka an induction
principle. Except that a fold (otherwise known as a weak rule-induction
principle) isn't enough for programming with these things, because it
throws away information: look, you can't tell the difference between
the constant case and the symbol case! It's ok for running expressions,
for which you only need the type index, but what if your program's
result type depended on the expression? I'm halfway through an example
(based on something a bit simpler than lambda-terms), which I'll send
off in a bit...

But anyway, it's an interesting question. Do you think it might be
possible to translate programs written in a pattern matching style into
applications of this sort of elimination operator? Perhaps someone should
do a PhD about it...

Cheers

Conor

-- 
http://www.cs.nott.ac.uk/~ctm