On 21 February 2015 at 10:09, Matt Oliveri <[email protected]> wrote: > > 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. >
Indeed. Lets forget this sub-discussion. > > > 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? > Given: g :: Nat -> Nat -> Nat g 1 2 At the application site of g we infer the type g :: fn' Nat Nat -> 'a where we want to allow definitions of 'g' that are more-curried. The relationship between the application type and the imported type is subtyping with fully-curried as the top type. However when typing higher order functions more curried is the bottom type for contravariant arguments. Hence why we can't agree on the order. It seems the behaviour is covariant with subtyping such that fully-curried is the top type. > > 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. 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. > 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. Indeed, in compositional typing the middle is where two code/AST fragments are joined. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
