On Thu, Nov 24, 2011 at 03:01:49PM +0000, Costello, Roger L. wrote:
Hi Brent,
Thanks for the feedback.
data Var = V | W | X | Y | Z
data Lambda = Variable Var | Application Lambda Lambda | Abstraction Var Lambda
Unfortunately, that's not quite correct. The first argument of Abstraction must be a Lambda term, specifically Variable Var.
No, that isn't possible (and it also doesn't make sense). It isn't possible because there is no way to express "this field may only contain values built with such-and-such constructor".* It doesn't make sense because why must the first argument of Abstraction be a lambda term? You yourself said "Abstraction of a Variable in a Lambda term" -- it is not "abstraction of a lambda term in a lambda term", but abstraction of a *variable*. Variables have type Var. Hence, Abstraction Var Lambda (I can also use an argument from authority: I have coded many variants of the lambda-calculus in Haskell, and I can tell you that this is the way it is done. =) -Brent * Actually, it is sometimes possible to encode this using GADTs. But that wouldn't help you here.