Currying/uncurrying of function arguments in Core.Stripped

[lukaszcz]

It is necessary that arguments provided to a function in an application be "curried" or "uncurried" to match the number of arguments according to the corresponding function argument type (unless the argument type is dynamic). For example, given

f : ((* -> *) -> * -> *) -> * -> *
g : * -> *

the application f g should be converted to f (uncurry g) where

uncurry : (* -> *) -> (* -> *) -> * -> *
uncurry g x y = g x y

This guarantees that in the call to g inside uncurry the general dynamic call method (CallClosures / ccall in JuvixAsm) will be used instead of the static call method (call in JuvixAsm). The dynamic call method checks the number of arguments at runtime, while the more efficient static call method must know the exact number of expected arguments at compile time. The static method can then still be used in the body of f because the argument uncurry g expects the right number of arguments. Note that g need not be a function -- it can be an arbitrary expression of the given type. The f and g above could easily result from erasing the types of polymorphic functions, e.g., they might originate from

f : {A : Type} -> ((A -> A) -> A -> A) -> A -> A
g : {A : Type} -> A -> A

The alternative would be to always generate general code which checks the number of arguments at runtime (unacceptable).

This transformation should be done after the types have been partially erased (see issue #1512), probably as a simple pass on the Core.Stripped data structure. Note that full type inference is not needed here -- just simple type inference on Core.Stripped which is straightforward to implement.

Examples

• The application

  map : (* -> *) -> List -> List
  f : (Nat -> Nat) -> Nat -> Nat
  
  map f lst

  should be transformed to

  map (curry f) lst
  
  curry : ((Nat -> Nat) -> Nat -> Nat) -> * -> *
  curry f x = f x

  Then the call to curry f with one argument will create a closure of f with one argument. A static call to f with one argument is erroneous, because f expects two arguments. The compiled code for the above will allocate a closure because the translation to JuvixAsm can see that fewer arguments are supplied than expected. This information is lost when f is passed as an argument to another function and called with the static call method in that function.

• The application

  id : * -> *
  f : ((Nat -> Nat) -> Nat -> Nat) -> Nat
  
  f id

  should be transformed to

  f (uncurry id)
  
  uncurry : (* -> *) -> (Nat -> Nat) -> Nat -> Nat
  uncurry id x y = id x y

  Then uncurry id can be called with two arguments. A static call to id with two arguments is erroneous because id expects one argument. The compiled code for the above will use the dynamic call method for the call to id because the translation to JuvixAsm can see that more arguments are supplied than expected. This information is lost when id is passed as an argument to another function and called with the static call method in that function.

• The application

  f : * -> *
  g : Nat -> Nat
  
  f g

  should not be transformed. Since the argument type is dynamic, any calls to it inside f will be compiled to use the dynamic call method (which is much less efficient but always correct).

Dependencies

• Issue Remove type arguments and type abstractions from Nodes #1512.
• Issue Translation from Core to Core.Stripped #1520.
• Closing Parse optional type information in JVC files #1509 would help with debugging.

[lukaszcz]

This is a bit more complicated with closures stored in data structures or third-order functions.

For example, given

f : List (* -> *) -> List (* -> *)
l : List ((Nat -> Nat) -> Nat -> Nat)
f l

we would need to convert all functions in the list, and then convert them back.

For

f : ((Nat -> Nat) -> Nat -> Nat) -> Nat) -> Nat
g : (* -> *) -> Nat
f g

we would need to dynamically convert the argument on each call to g inside f.

I think the most reasonable way to see this is as a "specialising" optimisation, where we can statically determine the arities in most cases, but don't bother with the rare/complicated cases. In addition to the arity-specialised versions, we have a general version of each function that uses CallClosures for each call to an unknown function. We use the general version when the function is passed to a third-order function or stored in a data structure.

I think we should move this to 0.4 and for 0.3 just use CallClosures for all applications with variable head.

[lukaszcz]

Instead of converting the arities, we could just use the general versions of the functions whenever the arities don't match. This is perhaps more reasonable, because a call to a converted function may actually be less efficient than just using CallClosures, especially after implementing #1653.

[lukaszcz]

After implementing

• Improve closure calls in the runtime #2396

there seems to be no significant runtime difference between compiled Juvix programs using the specialised APPLY_N runtime macros and the manually written arity-specialised Juvix runtime programs. Hence, implementing arity specialisation is probably not worth the effort when we have:

• Improve closure calls in the runtime #2396
• Inlining #2036
• Specialization optimisation #2164

So I'm closing the issue.