On Sat, Feb 21, 2015 at 5:41 AM, Keean Schupke <[email protected]> wrote: > On 21 February 2015 at 10:09, Matt Oliveri <[email protected]> wrote: >> You could say that. I do think your order on types is a useful >> informal way to understand which specializations are sensible. I >> actually can't answer this in full accordance with Shap's proposal, >> since he uses arity variables, which I don't understand. > > Im not sure I would say subtyping is informal. I would say as it sticks to > core type theory, without directly invoking arities it is more formal.
I'm saying that the way I've been getting use out of your order so far has been informal. I'll give you the benefit of the doubt that you have a formal system in mind that uses it. Arities are perfectly formal too, just less "pure", or "core" as you say. But function types have explicit arity isn't so pure either. >> My way of thinking about it is that arity-abstract types are >> constraints on function types. The constraint essentially _is_ to be a >> subtype of the "natural" application type, using your order. But it's >> not subtyping, since this order is only used to constrain unification, >> not for subsumption. > > So what is it? This sound a lot more informal than my approach. It's type constraints. Not informal at all. It's actually kind of like bounded quantification, which might be a problem. But hopefully not, since it's not a general-purpose subtyping order for the whole language. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
