On 1 April 2015 at 18:23, Keean Schupke <[email protected]> wrote: > Hmm but that variable does not follow normal unification rules. Its not a > type variable, but looks like a kind of expansion variable? > This appearance is one reason that I am not in love with the arity list notation. But the arity list notation is merely a different way of writing the all-arrows-have-a-call-variable notation that I used, and *that* notation clearly falls within the realm of [extended] HM-style inference. It doesn't seem to me that merely writing the same information in a different syntax should be deemed to break unification.
Incidentally, the same idea appears elsewhere in the literature in the context of effect types. The heart of the problem in choose_one is that we do two term substitutions replacing a type variable with an arrow type, and in doing so we lose the correlation of effects on the two substitutions unless there is a variable of some form on the arrow that keeps them related. The analogous problem in effect types is to ensure that effects inferred from one substitution propagate correctly to the other substitution. In the presence of a variable on the arrow it works fine. In the absence of that variable it doesn't. The other point here is the discussion Matt and I had about whether we have an 'n' value. That would indeed lead to a non-HM mechanism, and as I've said elsewhere in this thread it is the reason that my version of the arrow variable only admits "unresolved variable" and "yes it's a call point". You never get the "not a call point" case in my scheme, because that can only be said with the CFN type. On Wed, Apr 1, 2015 at 4:56 AM, William ML Leslie < [email protected]> wrote: > On 1 April 2015 at 18:23, Keean Schupke <[email protected]> wrote: > >> Hmm but that variable does not follow normal unification rules. Its not a >> type variable, but looks like a kind of expansion variable? >> > > Unification is really the wrong word to describe what we are doing during > arity specialisation. Function types of concrete arity only unify with > themselves. Arity-abstract function types also unify only with > themselves. They may be specialised, in which case a substitution is > performed, but this substitution is not term for term but term for a > specific variable. > Yes. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
