Implement Labeled Tuples

[WondAli]

Labeled Tuples

Overview

This PR introduces labeled tuples to Hazel, allowing tuple elements to be named using the = operator.

Note: This PR replaces an outdated implementation on a different branch, as I couldn't change the source branch on the old PR.

What Are Labeled Tuples?

Labeled tuples allow elements within a tuple to be named using the = operator. For example:

(x=1, y=2)

Here, x=1 and y=2 define labeled elements. These labels are only relevant within the enclosing tuple. Conceptually, = acts as a binary operator that pairs a label (a string) with an expression.

Labeled Tuple Features

Labeled elements can appear in any order when matched against a labeled tuple type, while unlabeled elements must maintain relative order.

Examples

• (x=1, True, y=6) correctly matches the type (Bool, y=Int, x=Int).
• let x=a, b = (y=2, x=4) binds 4 to a and 2 to b.

Dot Operator/Projection (.)

The dot operator allows extracting labeled elements from tuples:

(x=1, 2, 3).x  # Evaluates to 1 #

Singleton Labeled Tuples

A labeled tuple with a single element, such as (a=1), follows the same principles as multi-element labeled tuples but has some unique characteristics:

• Syntactic Form:
  • A singleton labeled tuple is typically written as (a=1), but parentheses are optional, so a=1 is also valid.
• Type-Checking & Label Inference:
  • If an unlabeled value is analyzed against a labeled tuple type, it is automatically wrapped as a singleton labeled tuple.
  • Example: Analyzing 1 against (a=Int) infers 1 as a=1.
• Dot Operator Compatibility:
  • (a=1).a correctly extracts 1.

Implementation Strategy

Labeled tuples are implemented by extending existing constructs in expressions, patterns, and types:

• TupLabel: Represents a labeled tuple element in expressions, patterns, and types.
• Label: Represents the label itself, always appearing in the label position of TupLabel.
  • Any other sort present in label position other than a valid label or empty hole is placed in a MultiHole
• Dot: In expressions represents tuple label projection (i.e., field access). The right-hand argument of Dot must be a Label.

Automatic label inference

• Missing labels are introduced during the elaboration phase for tuples
• Singleton labeled tuples are converted to tuples during Statics and the syntax is rewritten and stored in the info map.
  • During elaboration this syntax is pulled out of the info map to rewrite the syntax before evaluation

Future work

• Introduce Label sort that keeps labels in their own syntactic context

[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?

[7h3kk1d]

Evaluation should continue around:

let x : (a=Int, b=String)= (a=1, b=? ) in (x.b, x.a)

[7h3kk1d]

There's another issue with the parsing for type annotations outside lets:

((a="Foo", b=8) : (a=String, b=Int))

[cyrus-]

• floating point exponential notation isn't working anymore
• see inline comments

[cyrus-]

check to make sure label positions are not being recursed into for variable mentions / recursive functions / etc.

[7h3kk1d]

@cyrus- since we don't have the label sort introduced, the variables in label position are still being evaluated:

I can try to make these indet, but it's not clear to me that it's preferable to stop dynamics for the expression. If we still allow evaluation I think we want to continue to recurse into the "label position" in SyntaxTest.

[7h3kk1d]

This seems somewhat related to decisions for now evaluation should proceed in non-empty holes #1497 (comment).

[7h3kk1d]

I've put everything in label position in multiholes if it's not a label.