Well, x and y should have different types:
x : [Nat -> Nat] -> Nat // indicating native arity with [] brackets
y : [Nat] -> {Nat} [Nat] -> Nat // indicating captured environment type with {}
brackets
choose_one : [A -> A -> Bool ] -> A
In f, you have to unify x and y, which in my opinion should fail – but if you
really want that unification to succeed, the type-checker can go in two
directions. Either, generate the function
y’ : [Nat -> Nat] -> Nat
y’ [n m] = y n m
Or, the function
x’ : [Nat] -> {Nat} [Nat] -> Nat
x’ n = \m . x [n m]
As you can see, with currying syntax you are essentially under-specifying your
intent. What is more is that you have hidden possible allocations (in the case
that x’ needs to be selected).
Again, I really don’t think this belongs in a system’s programming language.
PKE
From: bitc-dev [mailto:[email protected]] On Behalf Of William ML
Leslie
Sent: Tuesday, February 17, 2015 9:53 PM
To: Discussions about the BitC language
Subject: Re: [bitc-dev] Arity inference at call (application) sites
My concern, Shap, is that there are some cases where template instantiation
falls down, and one of those cases is where the meet operation or
let-polymorphism or branching does not adequitely describe the property you're
trying to maintain. I get that you can define how this native-arity inference
behaves at the function call boundary, but the interesting case is the one
where you combine two results into one. This is the case I want to pick your
brain on.
On 18 February 2015 at 02:03, Jonathan S. Shapiro
<[email protected]<mailto:[email protected]>> wrote:
On Mon, Feb 16, 2015 at 2:57 PM, William ML Leslie
<[email protected]<mailto:[email protected]>> wrote:
I'm a bit uncomfortable with what happens in the case of let-bound
native-arity-polymorphic case:
let f = choose_one x y z -- different arities
in f n m
How do you choose a native arity for the callsite?
In a sense, you don't. The arity of f is determined at its definition. In this
case, I cannot tell what it is, because I don't know what the return value of
choose_one is. But it cannot depend on the dynamic branch taken in choose_one,
because this isn't a lazy language.
Please: native arity. The arity of f is 2. It's the *native arity* we care
about - the number of arguments that will be consumed by the CALL instruction.
That is, weather evaluation proceeds as (bitc/call (bitc/call f n) m) or
(bitc/call f n m).
choose_one returns one of its arguments; and perhaps x has a curried definition
and y takes two arguments directly. They have the same type, of course, so
this is a perfectly reasonable thing to do. But then what instructions do I
emit to call f? It may need to be called twice or once, how do we tell?
The only reasonable answer is that choose_one makes a choice of arity for you.
But I can't figure out by your rules which arity it will choose. Simply
propogating the native arity of the original function couldn't work, because
the native arity of the selected function depends on a runtime value.
If you say "it's 2", the algorithm is overspecified. If you say that depends
on the dynamic branch taken in choose_one, you can CPS transform and pass *all
three* continuations.
I'm not understanding this statement. I'm not sure how a dynamic branch in
choose_one could yield a change in arity.
It could return functions with the same type but different *native arity*.
You don't know statically what the native arity of the defined function was.
I don't think you want to do that. Can we adopt a calling convention from
something like STG or FORTH?
No. We need to be able to do the hardware-preferred (or more precisely:
conventional compiler preferred) calling convention.
Have I misunderstood how you intend to compile this?
I suspect so, but I haven't done a very good job of describing it. I'll attempt
to correct that in just a little bit.
It's this that I want to know about, that I still can't tell from your
description:
X_t = Nat -> Nat -> Nat
-- These are for illustration purposes only. In practice, they could be a lot
more complicated.
x, y : X_t
x n m = n + m -- native-arity = 2
y n = y' -- native-arity = 1, 1
where y' m = n + m + 1
choose_one : X_t -> X_t -> Bool -> X_t
choose_one x y z = case z of
True => x
_ => y
g z n m = let f = choose_one x y z
in f n m -- how many applications appear in the final 'in' clause?
why?
--
William Leslie
Notice:
Likely much of this email is, by the nature of copyright, covered under
copyright law. You absolutely MAY reproduce any part of it in accordance with
the copyright law of the nation you are reading this in. Any attempt to DENY
YOU THOSE RIGHTS would be illegal without prior contractual agreement.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
