On Mon, Mar 30, 2015 at 4:17 AM, Keean Schupke <[email protected]> wrote:
> I don't know if this is a difference in terminology or not, but: > > 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. This is why we need a distinguished arrow type, either written as a distinguished arrow or disguised within something comparable to the afn syntax. > So re-recap my representations: > > - A curried arrow (can only accept one argument) is used to represent > arity-abstract functions. We can call this an abstract-curried arrow if you > like "->" > > - An uncurried arrow (can have more than one argument) is used to > represent concrete-arity functions. We can call this a concrete-arrow "=>" > > After initial parsing arity abstract functions look like this: > > 'a -> 'b -> 'c > 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 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. > > And arity concrete functions look like this (and may return further > functions): > > 'a 'b => 'c > > After concretisation all (curried) arity-abstract arrows disappear, and > are no longer valid in the type system, only (uncurried) concrete-arity > functions remain. > I think this is just a different notation for the cfns we have been talking about all along. I'd urge you to stick with the cfn notation in this discussion thread so that we don't have confusion about the meaning of the => arrow (which already has a bound meaning in the present thread of discussion). shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
