| 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!
Simon
