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.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
