Just from my own sanity, here’s (my admittedly layman’s) summary of ideas from
this thread.
Shapiro’s type syntax for function (and closures), is fn arity tvar -> tvar ->
… -> tvar, so the arity is explicit (and can be bound as a variable).
Keean’s type syntax: fn tvar tvar … tvar -> tvar, so the arity is implicit (and
hence can’t be bound as a type variable).
Also, function types are used both in definitions and applications (function
calls). Shapiro has pointed out that function definitions has to be concrete,
since we’re interfacing with foreign modules of which we have no control. So,
assume that all function definitions are concrete and unalterable from now on.
Throughout the discussion, there’s been misunderstandings due to the
relationship with subtyping. Subtyping in this context (arity subtyping) is a
little unusual, in that it does not come up in most languages. In order to be
able to sub-type, the compiler has to be able to use a value of a type that is
a sub-type of another. So, for instance, if the compiler allows turning an
x:uint64 to a float64, and sqrt: fn 1 float64 -> float64, then `sqrt x` is
sound, since we can “cast” uint64 to a float64. We say that uint64 <: float64.
If we are given a function definition f : fn 2 ‘x ‘y -> ‘z, then it can be used
as a fn 1 ‘x -> fn 1 ‘y -> ‘z, by creating another function f’ (a trampoline
function):
def f’ x = lambda y { f x y }
The problem with this is that if we automatically generate this function, we’ll
introduce hidden closures that may allocate data, so we will disallow this in
the typing system.
One the other hand, if we have a function g : fn 1 ‘x -> fn 1 ‘y -> ‘z, we can
use it in contexts accepting a fn 2 ‘x -> y’ -> ‘z by using the function:
// For clarity, I will continue to use []-brackets to make the intent clearer.
def g’ [x y] = ((g x) y)
In this case, we do not have an allocation, hence we are okay with this form of
conversion. So, we can now give an example of our arity sub-typing rules:
a) fn 1 ‘x -> fn 1 ‘y -> ‘z <: fn 2 ‘x -> ‘y -> ‘z
b) The converse is not true (but only if we disallow it due to allocation
concerns).
Now, even though we can coerce a curried function to a non-curried one, it
doesn’t mean that it is well defined. For instance, if there’s many ways of
coercing a uint64 to a float64, then we have a problem picking out the correct
coercion. In some contexts, we do not have the target arities at hand [because
we are in an arity-abstract function], and because of b) we have to be careful.
Keean suggest that we can take any term [g a b c d] and type it as fn 4 ‘a ->
‘b -> ‘c -> ‘d -> ‘e, but that would be wrong, because if g later happens to
have arity less than 4, then we’ll have to resort to the disallowed coercion.
The most conservative approach would be to type it as fn 1 ‘a -> fn 1 ‘b -> fn
1 ‘c -> fn 1 ‘d -> ‘e, but we don’t want that either, because now we might end
up with too many allocating lambdas in the surrounding function. In order to
make sure we don’t end up in this situation, we have to make sure that when the
context specializes (at which point we do have proper arity bounds on all
functions), that we produce the most optimal function calls (applications).
So, it all boils down to if we have enough information at specialization time.
But note that if a function takes as arguments or return value general-arity
functions, we will not be able to get complete information. I think this is the
crux of the matter as it stands. I am not convinced that we can solve this
problem without resorting to disallow general-arity functions as arguments to
functions.
Thanks,
PKE
From: bitc-dev [mailto:[email protected]] On Behalf Of Keean Schupke
Sent: Monday, February 23, 2015 3:00 PM
To: Discussions about the BitC language
Subject: Re: [bitc-dev] Arity inference at call (application) sites
> Having defined this order on concrete-arity function types, we can say that
> the type at the call site must be a super-type of the definition type. This
> is really saying the same thing as the higher-order-function argument case.
Yes, this all falls out of contravariance for argument types.
Maybe i'm not stretching it at all then, if its obvious form contravariance? In
any case, hopefully the idea is clear.
Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
