On Sat, Feb 21, 2015 at 2:57 AM, Keean Schupke <[email protected]> wrote: >> Constraining what function? (fn 'a 'a -> 'a)? It makes no sense to >> constrain that, since it's already a concrete function type. > > Type class constraints also indicate membership, so it is an instance of > "Arity 2", even if it is not necessary, it is not wrong for it to be a > member.
If you think "Arity 2" is a type class, then the type "Arity 2 => fn 'a 'a -> 'a" is something like "Monad => [a]" in Haskell. That wouldn't make sense would it? Let's take a step back. Why did you come up with your own syntax for whatever this is, if your proposal doesn't use it? >> I think there's been a misunderstanding. There's no such thing as an >> abstract arity. Shap's proposal uses arity-abstract types, which have >> had the (concrete) arity abstracted out of them. > > There is obviously such a thing as we can sum all the components of an arity > as in: > > (1, 1, 1) = Arity 3 > (2, 1) = Arity 3 > (1, 2) = Arity 3 > (3) = Arity 3 OK, now I know what you mean by "abstract arity" though that's probably not a good name for it. This is not part of Shap's proposal, I'd say. The closest thing is that the arity-abstract type inferred from an application indicates the maximum arity that compatible function types can have. > In any case, abstract-arty types that have the arity abstracted out do not > represent the same thing as a subtyping hierarchy with fully-curried as the > super type. That's for sure. You got it backwards again; uncurried is the supertype. But arity-abstract types is different from subtyping, period. So what are you arguing by pointing out this difference? >> In Shap's proposal this is a unification error. (f 1) constrains the >> type of f to have an arity of at most 1. I currently don't understand >> the details of the notation, so I don't know how you'd read that >> constraint from a type, but here we can infer it. But f has arity 2. > > Okay so there is no difference here. We both think it should return be a > type error. > >> > The other way around, applying more arguments to a curried function is >> > trivial to see requires no additional allocations. >> >> Right, and Shap's proposal is designed to allow that. > > Without a subtype hierarchy, I don't see how the abstract-arity type only > admits less-curried applications? Is there some kind of implicit subtype > hierarchy? 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. 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. I have been thinking about how your type order makes the combination of definition-driven arity specialization and application-driven arity specialization easier to understand. In definition-driven, you move the application down the order toward the definition; in application-driven, you move the definition up the order toward the application. Of course it now seems sensible for them to meet somewhere in the middle. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
