On Tue, Feb 17, 2015 at 8:53 AM, Jonathan S. Shapiro <[email protected]> wrote: > OK. Let's see how much of a concrete proposal I can capture before my next > appointment. Note: I need *some* concrete syntax to talk about this, so > let's not complain about concrete syntax. I don't love it either. > > When I write "arity-k", I mean a function taking k arguments and returning 1 > result. > > The proposal requires that there are arity-abstract function types and > arity-concrete function types. As a working syntax for discussion: > > 'a -> 'b -> 'c is an arity-abstract function type. It is unspecified > whether this is a single procedure taking two arguments or a procedure > taking one argument returning a lambda having type 'b -> 'c. When function > types are inferred from an application, an arity-abstract function type is > inferred. > > fn 'a 'b -> 'c is an arity-concrete function type. This is known to be a > procedure taking two arguments. > > Function definitions and declarations (both top-level and local) are always > assigned an arity-concrete type. This is done in "what you wrote is what you > get" form. Thus: > > def f x y = x + y > f :: fn 'a 'a -> 'a > > > def f x = lambda y { x + y } > f:: fn 'a -> (fn 'a -> 'a) // parens not actually needed here. > > > The *parameters* and the *return type* of a function may have arity-abstract > type: > > map:: fn ('a -> 'b) (list 'a) -> (list 'b) > > > Note that *because* function definitions and declarations are always given > an arity-concrete type, the only place that arity-abstract function types > can appear is at function parameter types. Ultimately, a function parameter > type on a function that is actually called is necessarily passed a concrete > function (though this may proceed transitively). The arity-abstract function > type is specialized to an arity-concrete function type as a consequence. > > An arity-abstract function type 'a -> 'b -> ... 'z is specialized to an > arity-concrete function type fn 'a 'b -> 'c as follows: > > 1. For an arity-concrete function of arity k, there must be at least k types > appearing to the left of the final arrow of the arity-abstract type. This > ensures that specialization does not introduce a requirement for lambda > injection. Informally: the sequence of actual parameters must be "long > enough." > > 2. The first k types of the arity-abstract function type must unify with the > k argument types of the arity-concrete function. > > 3. Any remaining portion of the arity-abstract function type must unify with > the result type of the arity-concrete function. > > 4. Specialization proceeds left-to-right. That is: an arity-concrete > function type is first matched against the leading portion of the > arity-abstract function type, and then the remainder of the arity-abstract > function type is matched against the return value of the arity-concrete > function type. > > > Note that the first rule means that > > fn 'a 'b 'c -> 'd > > > does NOT successfully specialize the abstract function type 'a -> 'b -> 'c, > because an insufficient number of arguments is present. > > > OK. I'm sure there are a hoard of things that I have managed to leave out > yet again, but hopefully this is concrete enough that we can move toward > having a common conversation about it.
This all makes sense to me, and seems like it would work. The main issue I see is that arity abstract functions are not first class in that they can't be stored in data structures. That makes certain kinds of functionality programming less intuitive, since it means libraries designed around arity abstract functions would force users into somewhat unintuitive allocations for many kinds of callback code (even if these allocations were explicit). Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
