Singleton Labeled Tuple in Let Expression

[Negabinary]

I think m here should just be a singleton labelled tuple rather than an int

[7h3kk1d]

We do automatic label introduction for patterns the same as in expressions based on the type. We talked about this somewhat here #1235 (comment). We wanted the label introduction to work for higher arity tuples like let (a,b) = (a=1, b=2) in a (which seems to be broken) and for lambda patterns:

let f : (a=Int,Int) -> Int = fun (x, y) -> x * y  in
f(1, 2)

We could just disable singleton label elaboration for lets as another special case. @Negabinary @cyrus- let me know if either of you have thoughts or alternate approaches.

[Negabinary]

I think tuple autolabelling is confusing and the more special cases we add the more confusing it's going to get. I think it's important, both pedagogically and for the prevention of errors, to know whether something is a singleton tuple or just a value. I think the fact that these kinds of edge cases exist make me want to simplify the autolabeling logic even more.

Perhaps an unhelpfully extreme position but I would vote that we only do autolabelling on higher-arity tuple expressions (not patterns).

So these would work

let x : (a=Int, Int) = (1,2) in

let f : (a=Int) -> Int = 
  fun x -> x.a

and these would be errors

let f : (a=Int,Int) -> Int = fun (x, y) -> x * y  in
f(1, 2)

let x : (l=Int) = 8 in x

let f : (b=Float) -> Float = 
  fun b -> b
in ...

I just think anything else is going to get confusing fast

[disconcision]

impressive that this screenshot was captured within the 0.07 seconds it takes for the nut menu to fully unfurl

[7h3kk1d]

I have the same preference to remove singleton autolabelling all together. Removing autolabelling from patterns requires adding the labels for lambda params. That's also my preference but we would probably want an ocaml-style prefix operator for combining the label/binding. I'm not going to implement anything until there's some agreement on a plan as for this at least it is working as originally designed.

[cyrus-]

The main use for singleton auto-labeling is for function arguments and I don't want to require labels for single argument functions with a named argument. If you want to propose making function definitions and applications a special case for this and disabling it elsewhere, I'm open?

[Negabinary]

Singleton auto-labelling incurs a pretty big cost on our codebase and I'd like to suggest that it might not be worth it given where we are as a lab.

If I'm understanding correctly, the main point of auto-labelling is to make situations like the following shorter:

let f : (label=Int) -> Int =
  fun x -> x 
in
f(4)

saving writing out two occurrences of label:

let f : (label=Int) -> Int =
  fun x -> x.label
in
f(label=4)

I can see how this could be a nice convenience but it comes with some big conceptual costs on the codebase.

1. It breaks parametricity and the gradual guarantee. We already break these in a few places (numbers, reordering, sum constructors, n-ary autolabelling), but this one is a little more egregious because all of our other instances happen on very specific classes of terms. (you can only make a number expression switch from int to float using types). Singleton autolabelling goes a step further and allows any expression to change its semantics based on the type, and it's recursive in that the expression might be autolabelled multiple times.

The reason we want to keep as close to parametricity and the gradual guarantee is that straying from the path here adds frictions when we want to add more interesting editor features that involve replacing one expression with another. e.g. I think it should make proof steps involving replacements more complicated (though I haven't really thought about finding and fixing bugs like that yet), and I think @7h3kk1d 's wanted to eventually make structural refactoring tools that would be hit by frictions here. I think we can make more editor services faster if we avoid too much gradual guarantee breaking.

2. It changes the control flow of statics. Perhaps the best way to illustrate this is with the fact that everything else in statics takes place in one linear traversal on the expression tree (it sometimes traverses patterns twice, I'm pretty sure it only traverses expressions once). Specifically singleton auto-labelling requires an exponential (in the number of auto-labels) traversal of the expression tree.

This is because the logic of auto-labelling is that it 1) works out the type of the expressions before auto-labelling 2) checks if that type has the right label, 3) if it is missing the label, then it has to re-run the statics on an expression it has already run statics on with a different analytic type.

This friction is particularly salient given that we have two different attempts to rewrite statics upcoming, both the statics+elaborator combining on Hazel 3 that we all want but no-one quite has time to work on right now, and the incremental statics on Hazel 4. I would think both development efforts would benefit from simplifying the shape of our expression traversal.

3. I still think this is going to add confusion to someone trying to learn the language. This is admittedly more subjective, but I find the following examples' errors or lack thereof pretty confusing:

TL;DR I think it would be relatively easy to remove singleton auto-labelling from the codebase, that it wouldn't incur too much cost to the hazel programmer, and that it would reduce our frictions as developers to make more exciting features.

[disconcision]

fwiw ran into this one while demoing causing considerable confusion