Implement Labeled Tuples

[WondAli]

Goal: Implement Labeled Tuple functionality into Hazel.
Note: I don't think I can change the source branch on the old pull request. This redesign of the implementation was started on a new branch, so the old pull request (and branch) is outdated.

TODO: Add more detail to the pull request; add more detail about syntax and semantics

What are Labeled Tuples?
An element in a tuple can be "labeled" or "named" with the = operator. For example, (x=1, y=2) is a tuple expression in which its elements are labeled x and y respectively. These labels are relevant only within their nearest enclosing tuple.
The = operator can be thought of as a binary operator that takes in a string and an expression, and returns the expression.

(Uncertain) A labeled element is type-consistent with the type of the element it is labeling.

Labeled Tuple Features
When analyzed against a labeled tuple type, the labeled items can be placed anywhere in the tuple expression and tuple type (the unlabeled items must be in relative order to each other).

• Ex: (x=1, True, y=6) is properly typed against (Bool, y=Int, x=Int)
• Ex: Let x=a, b = (y=2, x=4) will bind 4 to a and 2 to b

Dot Operators
The dot operator . can be applied to a tuple to extract a labeled element.
For example, (x=1, 2, 3).x is equivalent to 1
Currently undefined for anything except tuple expressions.

Implementation Strategy

1. Implement a "label" term to express the labeled tuple element.
2. Modify tuple semantics to consider labeled term contained within the tuple.
3. Implement the dot operator as a new expression that takes an expression and a pattern (var only)
4. Modify labeled tuple semantic interactions with let-binding, casting, function application, etc.

Checkpoints:

• finish writing the draft pull request
• Implement the Label term that simply wraps an element with a string.
• Tuples type-check assuming all elements are in order.
• Tuples type-check considering rearrangements of labeled elements.
• Tuple type-checking when there is an unequal number of labeled elements
• Dot operation on Tuple expressions
• Labeled tuples as function arguments
• Code Cleaning and Optimization
• Add documentation buffer for labeled tuples
  Known Bugs:
• Label uniqueness in a tuple needs to be checked during statics (currently dynamic check is broken too?)

[cyrus-]

@WondAli playing with this branch, looks like the labels aren't showing up in the types of the tuples (and so you get weird run-time errors when projecting out a label that doesn't exist). is there a specific issue with adding labels to product types?

[cyrus-]

• singleton analytic case for patterns should insert labels

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

• better messages in the cursor inspector for when lifting occurs

[7h3kk1d]

Here's a first pass on the "better messages in the cursor inspector for when lifting occurs". We need to figure out how we want to represent this all in statics in a more disciplined way.

@WondAli let me know if you also have any ideas. If we move all the lifting/rearranging to statics maybe there's some additional data we can put on the Info.exp that can be used more generally.

[7h3kk1d]

Copying the status from the inner expression is probably too clever. We may need to have a more principled status for this expression.

[7h3kk1d]

• singleton analytic case for patterns should insert labels

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

@cyrus- I'm working on the pattern case now and I'm running across an issue I'm curious if you have thoughts on. In the following case the x pattern is getting expanded to (a=x) as it would in the function case so x ends up just being 3. So I'm kind of unclear how you actually would bind a variable to the singleton labeled tuple.

let x : (a=Int) = (a=3)

[cyrus-]

Ah I see, yeah that's awkward. Don't have an immediate solution...

[cyrus-]

Maybe only patterns that are not under an ascription have the lifting behavior? That would also allow you to explicitly bind a 1-tuple when defining a function:

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

and

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

seems natural enough to me.

[7h3kk1d]

Maybe only patterns that are not under an ascription have the lifting behavior? That would also allow you to explicitly bind a 1-tuple when defining a function:

This is implemented in the latest commit.

[7h3kk1d]

There has to be a better way to do this.

[7h3kk1d]

Something in the elaboration for tuples is adding a bunch more casts here