Implement 'Let Arguments Go First' about pikelet HOT 13 CLOSED

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...

from pikelet.

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!

from pikelet.

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

from pikelet.

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.

from pikelet.

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!

from pikelet.

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.

from pikelet.

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.

from pikelet.

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!

from pikelet.

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!

from pikelet.

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. 🤔

from pikelet.

@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. 😅

from pikelet.

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!

from pikelet.

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

from pikelet.