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. > We agree that arity-aware types break paretricity right? > Are you referencing my statement earlier? I meant that "full concretisation" - that is, resolving the arity of all type variables - this breaks parametricity. In exemplar, it's perfectly fine for b to turn out to be a function type in `map : (a -> b) -> list a -> list b` and we should not compile map differently just because this might be the case. A and b are just none of map's business save for size in the unboxed case. -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
