Proposal: rewrite application typer

[lepoetemaudit]

Overview

The current function in alpaca_typer that handles function application is really messy and hard to follow (largely my fault) and has some deficiencies, most notably when you pass 'too many' arguments to a function, which in fact is a function that returns a function that would accept the remaining arguments. I propose to rewrite this to be simpler, cleaner and correct these issues.

New approach

First, we see if there is a function available for that symbol that has been typed. If there isn't, we attempt to type all available functions for that symbol name. If there aren't any symbols at all, we abort with an appropriate error.

Secondly, we attempt to see if the application would result in an ambiguous curry. This would be for example:

let f x y z = x + y + z
let f x y = x + y

-- Is `f` here `f/2` or `f/3`???
let use_f () = f 10

In this case, we abort with an appropriate error.

Once we have selected tne most appropriate function to type against, we apply as many arguments as we can to it, and type the result. If we do not have enough to fully satisfy the selected function, we return the resulting curry. If we have just enough, we return the resulting type. If we have remaining arguments, we check that the resulting type is a t_arrow. If it is not, we return an error stating that $type cannot be applied, and that too many arguments were probably supplied (this is how Elm reports this error, for example). If the resulting type is t_arrow, we use the new resulting t_arrow and continue as before, applying arguments until there are none remaining.

We should be able to express this simply and recursively. At the code generation stage, I imagine we will need to break down each function that returns a function into a synthesized var before reapply remaining arguments to it, not too dissimilar to how we generate the curries.

Desired outcomes

• Much cleaner code
• The ability to pass arguments directly to functions that return functions, e.g.

type attr = Attribute (string, string)
type node = Node (string, list attr, list node) 

let element name attrs nodes = Node name attrs nodes

-- N.b. we still need at least a single argument - zero arity funs are disallowed even if  they are just curries
let div attrs = element "div" attrs

-- Currently produces an error stating that there is no function `div` of arity 2
let use_div = div [] []

[lepoetemaudit]

@j14159 happy to look at doing this myself (probably once you've completed the ETS work in the typer) but wanted your feedback / consent before doing so.

[j14159]

Seems to make sense to me. Am I correct in understanding that a change we'll see is that we will no longer try to find the most appropriate function from a set of functions with different arities? Are you thinking of requiring explicit arity references to solve this, e.g. f/2 2 3 per your example above to correct the ambiguity error that would occur with f 2 3?

[lepoetemaudit]

@j14159 I think my formatting / explanation let me down; I really like the current currying semantics and wouldn't seek to change those. Practically speaking the main difference I'm proposing is that if there are more arguments specified than would fit any functions available, we wouldn't reject it but would try and unify on the basis of the return value, but I don't want to add more special casing and branching to an already bloated function (which I largely bloated with the currying).

The new approach really boils down to walking through the function and the arguments one by one. We could think of it as pretending that functions are curried while typing them, so if it happens that the function ultimately returns a function, the walking algorithm just carries on typing against the supplied arguments. The behaviour would be similar to now, except that you wouldn't require parens to apply outstanding arguments to a function that returns a function.

[j14159]

OK, makes sense, thanks for clarifying. Honestly I could go either way on the need for parens but I think what you're suggesting makes some sense in terms of expressiveness.

All of this makes me think we might want another switch or option for the compiler to reject multi-arity functions if people don't like that. Similar to forcing decidability.