Improve support for lambdas

[GuiltyDolphin]

Something I might want to work on a bit once my exams are over. Raising an issue so y'all can provide some feedback, if you'd like (or tell me this is a terrible idea 😉 ).

Lambdas be Buggy

Currently, support for lambdas is buggy, and a great deal of programs I write which use lambdas will crash when type-checking. What's more, there are a couple of places we attempt to convert definitions to lambdas for localised use (but the code for doing this is duplicated and inconsistent).

First: Better lambdas

The first thing I propose to do, is to greatly improve the type-checking for lambdas---they are such a useful construct (and fundamental!), that writing programs without full support for them feels somewhat clunky.

Second: ... More lambdas?

The second thing I am wondering about, is whether we want to move to using lambdas more---we already have some (somewhat disparate) methods of wrangling our multi-parameter functions to lambda-form, so might it make sense to utilise these more when e.g., type checking. The underlying theory doesn't have multi-parameter lambdas (AFAIK), so it might make sense to convert to a lambda-form to bring some easier reasoning from the theory?

I know this might be a bit odd with e.g., line/column numbers (but hopefully we can preserve these anyway), but perhaps it might make sense to take e.g.,

foo : Int -> Int -> Int
foo x y = x + y

And instead of checking each equation individually, type-check the lambda-form:

(\(x : Int) => \(y : Int) => x + y) : Int -> (Int -> Int)

We can then focus more on how case/abs constructs are type-checked, rather than separately dealing with equation pattern matching (would be handled in 'case'), and functions would generally be type-checked as abs.

EOR

Ramble over, for now. Let me know if you have any thoughts.

[buggymcbugfix]

I believe we are using equations for top level because (in the general case) doing case is complicated w.r.t. specialisation induced by GADTs. I believe we only allow a grade to be specialised by a GADT pattern match in top-level equations.

I believe Idris tries to solve this by rewriting all cases to top-level definitions (as of Edwin's last visit a few months ago).

[buggymcbugfix]

PS: I am not happy (hehe) about your suggestion to do any rewriting in the parser! We should work towards parsing into a concrete syntax tree which reflects exactly the structure of the source file (ideally even maintaining comments and whitespace). We can then go crazy with rewrite passes on this to produce an abstract syntax tree that is worthy of its name.

I am imagining a pipeline that goes something like this:

Text
|
| parse
v
CST
|
| rewrite
v
AST
|
| check
v
Elaborated AST

[GuiltyDolphin]

Hmm, yes, I agree with the (lack of) rewriting in the parser—with the rewriting to the AST afterwards :)

I really like your suggestion of having a CST w/ comments—then rewriting to the AST!

I'm removing that query from the OP—for those interested, this was the original query:

Begin Query

Could we rewrite in Happy?

Just a thought, might we even be able to perform this rewriting in Happy, whilst parsing? So in this manner, we don't need to have additional [Equation]s for Defs, but instead perhaps a Def is just a named, typed expression?

E.g.,

foo : Int
foo = 7

bar : forall {a : Type} . a -> a
bar x = x

Might be along the lines of...

foo = (7 : Int)

bar = (\(x : a) => x) : forall {a : Type} . a -> a

End Query

Re rewriting to definitions: do you think we should do a similar thing, and rewrite cases to definitions w/ patterns?