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