Aritycheck

[crusso]

• enable arity checking in the interpreter
• revamp async lowering to produce n-ary replies as well as n-ary messages.
• prelude's (unary) new_async no longer returns a shared reply message but a local function to be called by an arity raised, shared reply message constructed by the compiler. This avoids a second trip through the scheduler on reply.
• cleanup
• tests
  (NB: there is a lingering bug (in the typechecker) due to functions taking unary tuples receiving the same flattened type as a function taking a single argument, still working on a fix but I think the correct thing to do is to either revamp the type-checker to deal with n-ary args/results or simply rule out unary tuples for now)

[nomeata]

(NB: there is a lingering bug (in the typechecker) due to functions taking unary tuples receiving the same flattened type as a function taking a single argument, still working on a fix but I think the correct thing to do is to revamp the type-checker to deal with n-ary args/results or simply rule out unary tuples for now)

Not sure I fully follow. Is there an example for that bug?

[nomeata]

Looks, good, only small suggestions!

[crusso]

(NB: there is a lingering bug (in the typechecker) due to functions taking unary tuples receiving the same flattened type as a function taking a single argument, still working on a fix but I think the correct thing to do is to revamp the type-checker to deal with n-ary args/results or simply rule out unary tuples for now)

Not sure I fully follow. Is there an example for that bug?

Yes, I've checked this in as test\bugs\aritybug.as:

// fails in the interpreter at line * with  ../../src/asc -r  u.as
// fails in the interpreter at line * with  ../../src/asc -r -a u.as
// but succeeds  ../../src/asc -r -a -A u.as

// the problem is that the type-checker accepts line * because  (Int,) and Int domain types
// aren't distinguished after arity raising, since Type.as_seq Int = Type.as_seq (Tup[Int]),
// eventhough Int != Tup[Int]

{
let t = "u_u\n";
shared func fu_u(a:Int,) : async (Int,) {
   return (2*a,);
};

let _ : async (Int,)  = async {
  let (x,) = await fu_u(1); // *
  assert(x==2);
  print t;
  return (x,);
};
};

[nomeata]

Oh, we actually have syntax for unary tuples? I thought we did not, and hence assumed this problem would not aryse arise. Now I know more :-)

Do we need syntax for unary tuples?

Is the problem due to the domain or the codomain of the function, or does it occur in both?

I think the solution is the following: When determining the arity of a function based on the syntactic form of the declaration, we currently apply these rules:

• If it is a manifest tuple pattern (or type), it is n-ary according to the pattern.
• If not, it is unary.

I think the following rules will resolve the issue:

• If it is a manifest tuple pattern (or type), and it is not a unary tuple pattern (or type) it is n-ary according to the pattern.
• If not, it is unary.

This enforces that we will have FuncD (_, _, [TupT [_]], _) in these cases, and everything works out. But we should maybe merge this PR and resolve this in a separate issue (either by removing the syntax for unary tuples, or by the above fix for the calling convention determination, or maybe some other way).

I guess one “other way” is to make TupT [t] = t in the type checker, but I am not advocating for that.

[crusso]

Yes, I was thinking along those lines too. We just want to ensure that the encoding doesn't identify types that should be kept distinct. On the other hand, unary tuples seems useless to me thought the unformity is nice.

[nomeata]

When compiling flatten-awaitables.as, I come across a case of CallE with a calling convention with an n > 1, where the argument is a manifest TupE, but this tuple has a length ≠ n… Weird, wouldn’t the interpreter complain about such things?

Ah, no, I guess it only checks that the calling conventions match, but it still happily passes values that don't fit the calling convention. So it looks like there is a type error in the translation somewhere.

[nomeata]

Ok, indeed the interpreter sees the problem. On my branch for n-ary function calls, I extended the interpreter to check this (I will remove this before merging, as it is likely too much debugging related cdoe for Andreas’ taste, but until the bug is fixes this is useful).

You can get the check onto your own branch using

git cherry-pick 774b8c5394231dde768fe75da277c414f22e172a

It only triggers in flatten-awaitables.as and says:

(unknown location): fatal error, Failure("calling convention (shared  2 -> 0) cannot handle non-tuple value func"

so you are trying to pass a single func to a binary message.

[nomeata]

Let’s make sure not only the calling conventions match, but also the actual arguments match the calling convention.

[crusso]

Bugger, I'll investigate.

[nomeata]

Investigating a bit myself.

• This fails:

  let a = actor { n0(u:()):async() {return ()}; };
  let _ = async { let () = await a.n0(); };
  

• while this succeeds

  let a = actor { n0(()):async() {return ()}; };
  let _ = async { let () = await a.n0(); };
  

• and this too:

  let a = actor { n0():async() {return ()}; };
  let _ = async { let () = await a.n0(); };
  

In the second and third case, the type checker gives this type to the function: shared () -> async () (Which is surely fine the third case, and a bit fishy in the second case), but in the first, failing case, it gives shared (()) -> async ()), which seems to be wrong, given that a.n0() is well-typed in all three cases.

I believe the problem is rooted somewhere deeper than your translation, and is related to the confusion around unary tuples, function taking no tuples, etc. Let's discuss that at #113 and then come back here.

[rossberg]

I'm having more and more second thoughts on the whole n-ary function type thing. It has become rather complicated and its failure to represent the unary tuple type consistently is a red flag as well. I wish I had thought of that earlier.

We had considered the flag alternative before, which would not have this problem, though perhaps others. Here is a third, maybe more systematic idea: we introduce an Unboxed type constructor. Then

  (Nat, Nat) -> (Nat, Nat)     ~>    Unboxed (Nat, Nat) -> Unboxed (Nat, Nat)
((Nat, Nat)) -> ((Nat, Nat))   ~>            (Nat, Nat) -> (Nat, Nat)
          () -> ()             ~>            Unboxed () -> Unboxed ()
        (()) -> (())           ~>                    () -> ()
      (Nat,) -> (Nat,)         ~>        Unboxed (Nat,) -> Unboxed (Nat,)
    ((Nat,)) -> ((Nat,))       ~>                (Nat,) -> (Nat,)
       (Nat) -> (Nat)          ~>                   Nat -> Nat

The Unboxed constructor of course is internal and can only be applied to types of internal kind Unboxable (which, for now, is the supertype of all tuple types -- edit: and of Async.). An Unboxed type itself has a kind that may only occur as arrow parameter result or as Async operand.

I believe this would avoid any discontinuity in the type algebra and be properly compositional. (Also related to #113.)

[nomeata]

Agreed that this became a mess.

When you write ((Nat, Nat)) on the left, what is that? Concrete syntax? Or abstract syntax? If the latter, is the outer thing a TupT [_] or a ParT _?

And will it be the case that func f(()) and func g() will have different types (Unboxed () -> vs. () ->), in contrast to what we had before?

Is there a semantic difference to the boolean flag approach (besides different trade-offs in implementation and data representation)?

The argument to a function can be unary (no Unboxed) or n-nary Boxed, right, and the compiler would look at the kind to determine the calling convention, and possibly the argument to Unboxed to determine the number of arguments.

Sounds all sound and doable. What I don’t understand yet: Why do we fail do to the following today properly:

  (Nat, Nat) -> (Nat, Nat)     ~>    [Nat, Nat] -> [Nat, Nat]
((Nat, Nat)) -> ((Nat, Nat))   ~>  [(Nat, Nat)] -> [(Nat, Nat)]
          () -> ()             ~>            [] -> []
        (()) -> (())           ~>          [()] -> [()]
      (Nat,) -> (Nat,)         ~>         [Nat] -> [Nat]
    ((Nat,)) -> ((Nat,))       ~>      [(Nat,)] -> [(Nat,)]
       (Nat) -> (Nat)          ~>         [Nat] -> [Nat]

I obtained this by composing your translation with this one (which is the translation the compiler would do):

Unboxed ts ~> [ts]
t ~> [t] -- where t is not Unboxed

In other words: What is the crucial property that makes the Unboxed approach different than plain n-ary function arrows? Or is there no such deep difference, but it its merely easier to get right?

[rossberg]

When you write ((Nat, Nat)) on the left, what is that? Concrete syntax? Or abstract syntax? If the latter, is the outer thing a TupT [_] or a ParT _?

It's concrete syntax, with ParT on the outside -- TupT [_] would be (_,).

And will it be the case that func f(()) and func g() will have different types (Unboxed () -> vs. () ->), in contrast to what we had before?

Yes.

Is there a semantic difference to the boolean flag approach (besides different trade-offs in implementation and data representation)?

I assume the end result is the same, but I think it factors it a bit nicer and less ad-hoc.

Sounds all sound and doable. What I don’t understand yet: Why do we fail do to the following today properly:
[...]
Unboxed ts ~> [ts]
t ~> [t] -- where t is not Unboxed
In other words: What is the crucial property that makes the Unboxed approach different than plain n-ary function arrows? Or is there no such deep difference, but it its merely easier to get right?

The difference is that (a) no case distinction is needed, making it uniform and avoiding compositionality hazards, and (b) we don't lose the information like your extra rule does, which fails to distinguish e.g. Unboxed (t,) from t.

[rossberg]

Note that this extends to async: a type T -> Unboxed (Async U) would be a "true" async function, whereas T -> Async U returns a first-class async value. Moreover, Async (Unboxed (T, U)) translates to a binary callback, while Async (T, U) remains unary.

[nomeata]

Sound good, ship it :-)

[nomeata]

In fact, we could use Unboxed in more places than function arrows and async. Return values in general (e.g. the body of a let) could be unboxed, which would avoid extra boxing. And we can box more things (Booleans, for example, words, maybe numbers in some way).

In other words, when t is something we can store on the heap, or as a pointer on the stack, then Unboxed t is something that is stored on the stack. I already see some nice things the compiler could do this way, e.g. compiling f (g x) with f binary would just work nicely. (I expect that this is far too implementation-guided thinking for your liking ;-))

This is just a glimpse of what we can do down the road eventually … but I agree that this goes in a good direction.

[nomeata]

we introduce an Unboxed type constructor

What about the term level: Would there be BoxE and UnboxE constructors? Or will that be implicit? (Explicit seems nicer to me at first glance…)

[rossberg]

I agree that we should have those on the term level. However, the question then is where to introduce them. The type ones could be introduced as desugarings in the parser already. But for the term level these are essentially implicit conversions that can only be introduced after typing.

Maybe we'll need to introduce a notion of implicit coercions after all?

[crusso]

I still think we are overthinking this. If we had simple type and syntax based distinction between second class sequences and first-class tuples we would be done.

Functions takes sequence patterns and return sequences, expressions produce sequences and tuple constructors take sequences and produce a singleton sequence that contains a tuple.Variables are never bound to sequences, only types, and functions are always applied to sequences and return sequences. Type range over types, not sequences. This is precisely what Kevin Mitchell does in his paper.

The current approach is flawed because we are trying to recover sequences from types that can be both non-tuples and tuples, blurring the distinction between plain values and singleton tuples.

[nomeata]

I would expect the type inference to add the terms level BoxE and UnboxE, as a form of elaboration.

Claudio, it seems that Unboxed (TupT ts) is nothing else but such a second class sequence. Can you clarify the differences some more? Would you make changes to the syntax?

[crusso]

Yes, I would just make changes to the syntax instead of being clever about it. JS users are familiar with parenthesized parameter sequences, AFAIK, not juxtaposition. So let's adopt that and add something like tup( e0,..., en) for first class tuples, or maybe (| e0,...,en |) (with symmetric pattern matching).

It seems to me that Unboxed is taking an arbitrary type, not a sequence of types - feels more like a type destructor than constructor to me ;-> but perhaps I'm just misreading it.