On Tue, Mar 31, 2015 at 7:09 PM, William ML Leslie
<[email protected]> wrote:
> On 1 April 2015 at 09:59, Jonathan S. Shapiro <[email protected]> wrote:
>>
>> I have answered this several times.
>>
>> f is a *parameter* whose only type information is a fresh type variable.
>> For example:
>>
>> def keean f a b c d tst {
>> if tst
>> f a b
>> else
>> f a b c d
>> }
>>
>> So no type signature of any kind for f, as I've said several times now.
>> The procedure definition above is all you have to work with.
>
> I thought that neither the Shapiro nor the Schupke scheme allowed
> underapplied functions? Ie, disagreement on the native arity of `f` is a
> type error.
There need not be a disagreement. For example if f has type (cfn 'a
'b->cfn 'c 'd->'rtn) both applications are well-typed. (That's not the
most general type.) We are not requiring explicit parens to separate
calls in Shap-based schemes, because technically we write
applications, not calls. The two applications require the type of f to
unify with (afn 'a 'b->'rtn) and (afn 'a 'b 'c 'd->'rtn) respectively.
Oh wait, that _is_ weird. Doesn't that violate the "occurs check" or
whatever? Because it asks for ('rtn = afn 'c 'd->'rtn)? Anyway, the
problem isn't the two applications of the same function themselves,
it's that they have the same type.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
