Hi all,
Continuing, still using the syntax where f[a b c] is a call (and not an
application), let’s define the problem. We want to translate all function
definitions in our program from a language that allows applications to one that
only uses function calls. This is a step towards creating assembly code, of
course, and at one step we have to get down from the high-level language to a
lower-level one.
I didn’t specify notation for the type of (primitive) function calls, nor
values of function calls. The value part is easy, all we store in memory is the
address of the function. I’ll also use a bracket notation for their typing:
1) Term: g [a0 a1 .. aN]
2) Type: f : [A*] => R, where A* is a list of type variables (space separated),
and R is the result type variable. The A’s and the R are general types, they
can be also be applications.
3) Value: Address of function in memory.
For (simple) applications, I will use the:
1) Term: g b
2) Type: A -> B,
Sometimes I will use A -{E}-> B, indicating the existential capture of the
environment E.
3) Value: A tuple (a, e), where a is a function call of type a : [E A] => B,
and e : E are the captured values.
You can see from this that A-{E}->B is isomorphic to ([E A]=>B, E), and
that
A->B is equal to: exists E. A-{E}->B.
Now, we are talking about different ways of translating our (lambda-like) input
language to one that does not have lambdas, nor applications, only let-bindings
and function-calls. Also, as an optimization, we want to make sure that if
there are n-applications (i.e. terms such as f a b c, and f :: [A B] -> R, then
it is translated to f [a b] [c].
In Shapiro’s proposal, all top-level function definitions will syntactically be
forced to produce a call, but their arguments and return value may be general
functions. Now meeting an application `g a`, if g : [A] => R (arity = 1), and
a: A, then g a : R. If g has more than one argument, then g : [A|Bs] => R, and
we can type it as g a : [Bs] => R and continue. If we end up with a type [Cs]
=> R we have specified too few arguments, and we should either error on it or
auto-generate a function (eta-conversion), or finally keep the eta-converted
function around in the environment, but error out if the function definition
escapes. Too many arguments is not a problem g a : [] => R, because it will be
type-checked against R. If R is a function (application or call) type, it’s
good, otherwise a type-checking error.
What is not so clear to me is how to proceed when g is a value if type A -> B,
for instance as provided as an argument to the top-level function. Or rather,
the main problem is that the type of a parameter can be A -> B -> C -> … -> R,
but we want to be able to call it with a concrete function f : [A B C … ] => R.
In this case, you would have to coerce the value f to another f’ that is an
applicative function (i.e. the tuple (a, e) above).
So, we need to expand on the simple applicative function values to more general
applicative function values:
1) Term: g a0 a1 … aN
2) Type: A0 A1 … AN -> R
3) Value: A tuple (a, e) where a : [E A0 A1 .. AN] => R, e : E.
Note: I’m contradicting myself here, but yes, you *can* sensibly talk about the
arity of a general applicative function – oops!
We can convert a primitive function value to general applicative function
value, by auto-generating the function
t : [f : [A*] => R] => (A* -> R)
t f = (\args . f [Nil args], Nil) -- We might not *actually* have to
generate this if the calling convention allows for a hidden environment
function argument.
Unification with simple application proceeds pretty much as primitive function
values. I haven’t proven it, but I’m pretty sure that it can work out, more
about that later!
Thanks,
PKE
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
