Simon Peyton-Jones <[EMAIL PROTECTED]> writes:
> | How about extending TC with a branch for abstraction:
> |
> | TC ::= ...
> | | /\a. TC -- abstraction
> |
> | This is too powerful and will get out of control -- we surely
> | don't want to give TC the full power of lambda-calculus. So let's impose
> a
> | restriction: in /\a.TC, a must occur free in TC *exactly once*. This
> | way, abstraction can only be used to specify with respect to which
> | argument a partial application is. (or I think so -- I haven't tried to
> | prove it.)
>
> That's an interesting idea that I've not seen suggested before.
>
> Someone should study it!
I wonder if the linear logic folks have studied this form of lambda
calculus?
Carl Witty
