On Tuesday, March 31, 2015, Keean Schupke <[email protected]> wrote:

> On 31 March 2015 at 21:28, Jonathan S. Shapiro <[email protected]
> <javascript:_e(%7B%7D,'cvml','[email protected]');>> wrote:
>
> Just ignore that, it doesn't make any different to my argument, it just
> means where I list the possible types of the imported 'f' we would use 'a
> -> b -> c -> d' for a local (arity abstract) definition, or if you prefer,
> put the concrete calls at the positions you want to infer them from the
> lambdas in the definition.
>

How do I put in concrete calls using your notation? We do not know enough
to put in concrete function types yet. Concrete calls and concrete function
types are separate issues.

The two applications in the example:
>>
>> f a b
>> f a b c d
>>
>> Occur in the body OF THE SAME PROCEDURE. Thus, the challenge is to infer
>> a single abstract function type for f that satisfies *both* uses
>> simultaneously. You gave inferred types for the two applications
>> independently, but did not account for the need to reconcile them to arrive
>> at a single type for f.
>>
>> Matt and I don't think they reconcile without some ability to remember
>> which argument positions must have a call arrow following the argument
>> position. In particular the choose_one example can't be handled without
>> that.
>>
>
> I think I have demonstrated how it can be handled without. I would
> appreciate if you could find the problem with what I have suggested. It
> seems to work for me.
>

Since you haven't addressed how the typing works in choose_one, I don't
think you have demonstrated this at all. Please explain how choose_one
works.


> The imported type  of 'f' must unify with both of these, so valid types
>>> would be:
>>>
>>
>> F is not imported.
>>
>
> Again, whether f is imported or not is not relevant to my argument, so you
> can ignore that and read 'type inferred from the definition' instead of
> 'type defined in the import/export'.
>

The definition of f is not in scope. The only thing we know about f is
inferred from the application. It's a parameter, initially typed with a
fresh type variable and then refined by inference from the two applications
I gave.

shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to