> 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
It seems to me that all you want is a symmetric monoidal closed category,
the modalities are superfluous. You might want dummy parameters (thus
affine, rather than linear), in which case you want the weakening rule (a
final object.)
Dana
