On Tue, Mar 31, 2015 at 3:41 AM, Keean Schupke <[email protected]> wrote:
> On 31 Mar 2015 06:18, "Matt Oliveri" <[email protected]> wrote:
>> 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?
>
> I never said they won't come up, I said they had been reduced with the
> available constraints. "id" is a good example, in the module where we define
> id the argument type and return type cannot be reduced further. Perhaps I
> should have said after all unification of types in the current compilation
> unit has been competed.
Oh, is that all you meant. Well you fooled me. The problem with that
is a type variable will end up meaning a certain specific type at
runtime even if we never actually see that type during type checking
(of the current compilation unit). So in that non-literal sense, c
above could become (d -> e). Of course, this needn't be a problem, as
you say.
>> >> 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.
>
> No, these are arity abstract, we don't care about calls at all.
You are talking to the wrong quote level. You already disagreed with
Shap about that. :)
>> > 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.
>
> I think you are missing that the input language supports both arity abstract
> and arity concrete functions.
No, I didn't assume otherwise. Combinations of cfns and HM arrows are
not enough to express the necessary constraints. Please do look at the
example and consider what could happen in your type system.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
