I want to expand on my earlier response to Keean's "we broke HM". In point of fact, it *does* look like we broke HM the way I described things originally, but not because of anything we have done with abstract function unification or arity variables.
The place where we seem to have departed from HM is in allowing an abstract function type to be "specialised" or "instantiated" by a concrete function type. I've assumed (and said) from the first that the scheme does something quite weird at arguments. Given a procedure having type f :: a->b=>c int => y we're saying that we can invoke that procedure as f g 1 where g has type cfn a b => c. That's not just a unification or a specialization in the traditional HM sense. Further, we've said that the mere *existence* of an abstract arrow type means that the function isn't fully specialized. That is: we can concretize all of the argument and return types, but even after doing so the non-call-arrow arrows are still deemed to be abstract enough to quasi-specialize using CFN. That's the part that appears to step outside of HM, because it involves a very strange notion of parametric specialization. The legitimacy of the substitution is a bit easier to see after we note that cfn a b => c can be written as a -n-> b => c the only reason I introduced CFN in the first place is that I initially failed to (mentally) model the arrow variable. Once we have that, it's easy to see that the variable can resolve to 'n' or to 'y' in the usual HM way. If you wish, you can think of that variable on the arrow as having boolean kind, with the consequence that it can only resolve to type-level-true (this is a call site) or type-level-n (this is not a call site). shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
