Implement 'Let Arguments Go First'

[brendanzab]

It would be nice to improve the bidirectional type checking algorithm to also pull information from the arguments. This could also help us eventually implement implicit arguments (see #8). A nice approach for doing this was given in the paper Let Arguments Go First. In the introduction the authors state (emphasis added):

We believe that, similarly to standard bi-directional type checking, bi-directional type checking with an application mode can be applied to a wide range of type systems. Our work shows two particular and non-trivial applications. Other potential areas of applications are other type systems with subtyping, static overloading, implicit parameters or dependent types.

In section 3 (the Hindley-Milner example) of the paper they show the application context pulling type information from the arguments in order to fill in the 'hidden type arguments' of the foralls via the subtyping rules. Perhaps we could do something similar for implicit arguments! This would effectively involve combining sections 3, 4, and 5.3 into one system.

Resources

• N. Xie, B. C. d. S. Oliveira, Let Arguments Go First. (Paper, Slides)
• C. Jenkins, A. Stump, Spine Local Type Inference. (Paper, Slides)

[brendanzab]

Ok, so I've been messing around with implementing this, but one issue that I'm running into is situations like Array 3 String. Because we overload numeric literals (ie. 3 could be U8, I8, U16, etc), these need to be disambiguated in a checking mode. But the rule for application in the paper requires the argument to be inferred first (hence the name of the paper!).

This seems to actually be annoying in practice, because it results in errors like:

error: ambiguous integer literal
- <test>:1:7
1 | Array 3 String
  |       ^ type annotation needed here

Really would rather not force people to write Array (3 : U64) String - ick!

[brendanzab]

Not sure if you have any thoughts on ways around this @xnning?

[xnning]

Thanks for your interests in our paper!

1. Let Argument Go First is not better (nor worse, though) than traditional bi-directional type-checking. Tradeoff is involved.
2. What's the type of 3? If you do something like x=3, what's the type of x? Or if you input 3 in an interactive environment, what's the type of it? Do user need to write type annotation for it?
3. Something like typeclass in Haskell might help. In this case, it can generate type Num a => a, and propagate the type info to Array, then solve the constraint (e.g.Num a => U64 ~ a)
4. Backtracking. This means we would have two typing rules from both directions

G | S |- e2 => A    G | S, e2:A |- e1 => B
---------------------------------------
G | S |- e1 e2 => B

e2 is not typeable
G |- e1 => A    G | S |- A <: B -> C        G |- e2 <= B
---------------------------------------------------------------------------
G | S |- e1 e2 => C

The drawback is that the performance might slow down.

Hope it helps.

[brendanzab]

Thanks so much for replying!

So here are some sample rules for integer literals n (as currently implemented in Pikelet):

G ctx
--------------------------
G |- n <= U8

G ctx
--------------------------
G |- n <= I32

G ctx
--------------------------
G |- n <= F32

I am planning to add type classes (like instance arguments in Agda: #13), so perhaps that might open up some different solutions. Good idea!

For now the backtracking approach seems like the simplest, so I might give that a go. Thanks again for your paper, it's been super interesting to play with!

[boomshroom]

In Haskell, integer literals are implicitly Integer, but if a literal needs to be a specific type, it calls fromInteger for that type. Meanwhile in Rust, untyped integer literals are assumed to be i32 unless inference requires a different type. Perhaps we could implement at least a short to solution of assigning a default type for integers.

In the long run, more advanced type inference will be needed.

[brendanzab]

Yep, this is what we were referring to when talking about the Num type class. It would certainly be nice to have overloaded integer literals, although there are limitations to Haskell's approach that it would be nice to see if we can avoid - for example it results in runtime errors on overflow.

I kind of don't want to assume I32, because then you'd get the error 'Array expected a U64' or something like that.

I do kind of like the idea of trying to limit the constraint solving as much as possible, because constraint solving tends to lead to more confusing errors. I also want any algorithm we pick to at least have some hope of being formalised! So we'll have to be careful about any additions we make.

[brendanzab]

Another neat approach that I've just come across is spine local type inference. I'm gonna press forward with Let Args Go First and the application mode, but I'm interested to see how much they have in common, and where they differ!

[xnning]

The spine local type inference paper indeed seems interesting. I am also curious about how much it have in common with let arguments go first (not much mentioned in the paper, though. let arguments go first is only cited together with many other approaches in intro). Would take a closer look. Thanks for pointing out the reference!

[brendanzab]

Yes, I wonder if it was a time pressure thing. Perhaps they didn't have much time to understand and compare it against your approach before publishing. 🤔

[brendanzab]

@xnning How did you go with the spine local type inference paper? I'm finding it to be a bit of a challenge to unpick! I kind of wish they gave descriptions of their judgement forms before jumping into their descriptions first. 😅

[xnning]

I don't have time to read this paper until recently. I totally agree that the mechanism and logic there are quite delicate and I had been confused by the inputs and outputs of each judgment for a while.
But somehow I think I got the main ideas now.
What I did is to read the paper again and again...

[brendanzab]

Hehe, yup! I have been going at it with a highlighter actually. It's not immediately obvious from the paper, and was clearer from the slides, but it seems like they solve the problem of using multiple directions in the arguments like I was struggling with above, which is super neat. I'd be interested to watch the video once it's released as well.

I just wonder if things could be simplified/clarified... perhaps playing around with the notation could help? One of the appeals of your paper that I could actually get my head around it!

[brendanzab]

Thinking instead I might go with constraint solving instead, more like in elaboration-zoo.