On Mon, Mar 30, 2015 at 7:16 PM, Keean Schupke <[email protected]> wrote:
> On 30 March 2015 at 15:08, Jonathan S. Shapiro <[email protected]> wrote:
>> On Mon, Mar 30, 2015 at 4:17 AM, Keean Schupke <[email protected]> wrote:
>>> On 30 March 2015 at 11:50, Matt Oliveri <[email protected]> wrote:
>>>> On Mon, Mar 30, 2015 at 2:54 AM, Keean Schupke <[email protected]> wrote:
>>>> > As such the function concretization pass only has to deal with fully
>>>> > determined arity abstract types.
>>>>
>>>> What exactly is fully determined about an arity-abstract type, whose
>>>> arity is--by definition--not yet determined?
>>>
>>> IE we know the whole type:
>>>
>>> a -> b -> c
>>>
>>> where c cannot be further expanded to (d -> e).
>>
>> Oh. Oh dear. I think you have a bad assumption. Even if we are doing
>> assembly-grain compilation, there are cases where we cannot know this. In
>> particular, we may be a consumer of a function supplied by some other
>> module/assembly whose type is 'a->'b->'c. In that case we don't know any
>> restriction on the potential expansions of 'c.
>
> And we don't care about future expansions either. Consider "id". We can pass
> a function to "id", and it returns the same function, whether
> arity-abstract or concrete. The only time we care if about the arity of the
> argument is if we actually do something that relies on it being a function,
> in which case the argument will not be a simple type variable, but a
> function type.
You seem to have just completely changed your story from "type
variables won't come up" to "type variables don't cause any problem".
Your new story makes more sense, but what the heck?
>> But note that we know something here that isn't captured in this notation
>> if we read it in the usual HM way. Specifically: we know that the final
>> arrow is necessarily a returning arrow where the preceding arrows are not.
>> I'm not opposed to this notation; I'm just pointing out that something
>> sneaky is being done here in the syntax. In particular, it means that
>>
>> 'a->'b->('c->'d)
>>
>> is not the same type as
>>
>> 'a->'b->'c->'d
>
>
> disagree, these are the same types.
>>
>>
>> the first says that there is a known return position after two arguments
>> are concerned. The second says there is a known return position after three
>> arguments are consumed.
>>
>> I'm not sure whether this was your intention or not. Clarification would
>> be helpful.
>
>
> My intention is that the 'usual' arrow is arity-abstract, and the semantics
> and type system behaviour is the same as in Haskell or other functional
> languages.
Thanks. But then you really are missing information that seems
necessary. For a concrete example where this could be a problem, see
my other email just now. Or Shap's email just now, with essentially
the same example.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
