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: > >> 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. > 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. > > This is why we need a distinguished arrow type, either written as a > distinguished arrow or disguised within something comparable to the afn > syntax. > I disagree, I don't care if a function returns a function, as long as I have enough arguments to make the call. > > >> 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 > 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. > > >> >> 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). > Which cfn notation? I don't like reusing the '->' arrow, as I want it to be easily visible that all arity-abstract functions have been removed after the concretisation pass. (cfn 'a 'b -> 'c) seems messy to me, if you don't like =>, how about: 'a 'b ~> 'c Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
