On Tue, Feb 24, 2015 at 2:57 AM, Keean Schupke <[email protected]> wrote: >> > Shap's proposal solves the problem. It allows arity-abstract functions >> > as arguments, and it never introduces allocations. It doesn't use >> > subtyping. > > So if its my description of the type system that is causing concerns perhaps > I can describe it a different way, and try and bridge the gap:
Is this an attempt at a self-contained proposal? In particular, are we free to forget everything you've said about your solution in the past? > - Infer an arity-abstract type for all functions: > > f x = \y . x + y > f :: Nat -> Nat -> Nat > - Infer a arity-concrete type for definitions: > > f :: fn 1 Nat -> (fn 1 Nat -> Nat) See, now you already did something weird. In your first bullet point, I assumed "function" was shorthand for "function definition". But now you're saying something different for definitions. And what's with that code? You just inferred two types for f. Why? > - constrain the arity-abstract type with an lower bound (the least type it > can accept): > > f :: (Nat -> Nat -> Nat) :> (fn 1 Nat -> (fn 1 Nat -> Nat)) In what circumstance are we to do that? Moreover, this proposal is not self-contained, since you haven't defined this order on types. And this isn't the old order on types either, since that one didn't relate arity-abstract types. > From the application infer an arity-concrete type: > > (f 1 2) > f :: (fn 2 Nat -> Nat -> Nat) So I'm assuming that's a different f, since you already inferred two types for the old one. > - constrain the arity-abstract type with a upper bound (the greatest type it > can accept): > > f :: (fn 2 Nat -> Nat -> Nat) :> (Nat -> Nat -> Nat) :> (fn 1 Nat -> (fn 1 > Nat -> Nat)) Oh, maybe not. Again, when do we impose this constraint? > - note the type is under-specified, and we can accept any type between (fn 2 > Nat -> Nat -> Nat) and (fn 1 Nat -> (fn 1 Nat -> Nat)), but generally we > prefer less curried as it will be more efficient. Hardly. It already has 3 types. Oh wait, you didn't really mean any of those types were the (native) type of f. They are just related to the eventual type of f. You didn't explain that well. > What about the other way around: > > f x y = x + y > ((f 1) 2) > > - would get the type: > > f :: (fn 1 Nat -> (fn 1 Nat -> Nat)) :> (Nat -> Nat -> Nat) :> (fn 2 Nat -> > Nat -> Nat) > > - but bearing in mind the order on types: > > (fn 1 Nat -> (fn 1 Nat -> Nat)) <: (fn 2 Nat -> Nat -> Nat) > > - this type admits no types (is a type error), which is what we want as we > cannot allow a lambda to be introduced into the definition of 'f'. This is also unclear. You suddenly flipped the direction of the order. Before you flipped it, it was indeed false. > Now the next step is to realise that the arity-abstract type does nothing, > it is the relation between the type required at the call site and the type > inferred at the definition that controls admission. In other words iff: > > inferred definition type <: inferred call-site type > > We are okay, and the abstract type part of the signature does nothing. Referring to the (strawman?) proposal in this email, you are right. Because subtyping is more flexible than arity abstraction. > However this type relation simply controls admission, and the compiler > implementation of keeping a partly compiled "abstract" version of the > function until it gets specialised at the call-site is exactly the same. But! If you admit things that Shap doesn't, you need to prove that they can be implemented without allocating. You fooled me; this isn't really your proposal. It's some rhetoric for why I should like your old proposal that you still haven't explained. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
