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.
> >> 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.
> > 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. For example, using my notation :
f : ('a 'b => 'c) -> 'a -> 'b -> 'c
Which I think Shap would write:
f : afn ? (cfn ['a 'b] -> 'c) -> 'a -> 'b -> 'c
Or something like that, I find it confusing, and I'm not quite sure...
Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
