Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

PHI 1 - Labeled Tuples #4

Draft
wants to merge 13 commits into
base: master
Choose a base branch
from
285 changes: 285 additions & 0 deletions 1-labeled-tuples/1-labeled-tuples.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,285 @@
# Introduction

<!-- TODO: what are labeled products -->
Labeled products are a value similar to products, but some/all elements have a label. This label can be used then for projection. This allows elements within the product can be accessed either positionally or by the label.
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
<!-- TODO: why do we want them in Hazel -->
Adding labeled products helps make the tuples become more robust, so more complex products can be easily used. Accesing a longer tuple using only positional arguments adds unneccsary bulk to the code. Having labels allows for easy access of values in a product. The labeled products can also serve a similar use as records in other languages.
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
<!-- TODO: what do we have now -->
Currently only unlabeled tuples are supported in Hazel, and elements can only be accessed positionally using let statements or case statements.
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
# Labeled Product Types
Syntax: `.label1 ty1, .label2 ty2, ..., .labeln tyn`

Files to Edit: UHTyp.re
<!-- TODO: add `.label` as a new type form <br/> -->
<!-- TODO: List the files you expect ot edit for each thing, and a sentance about what you expect to do -->
<!-- Just add space operator, check UHExp.re for this -->
<!-- Look at Skeltype parser and see that there is something that determines prescedence,-->
<!-- Stat that we are not requiring parenthesis-->

To add labeled product types, the operator and opearnd types will need to be expanded like so:
```
type operator =
| Arrow
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
| Prod
| Sum
| Space;
```
<!-- For space, say if left or right associative and give presedence-->
Space will be left associateive and have the highest precedence.
```
type operand =
| Hole
| Unit
| Int
| Float
| Bool
| Parenthesized(t)
| List(t)
| Label;
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
```

<!-- TODO: do we want to allow partially labeled product types? -->
Partially labeled product types are allowed, and labels and non-labeled positions can be interleaved.
For example, the labeled product type `(.x Num, Num, .y Num)` is allowed.

Singleton label products are supported. For example, `.x Num` is supported.

### Type Equivalence
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved

Bcause a labeld product may still be used with a positional arguments with partially labeld types, the type equivalence considers the order of the labels with equlivalence. For example, `(.x Num, .y Num, .z Num) != (.z Num, .y Num, .x Num)` because the order of the labels is different.


### Type Syntax Errors

* A label must be followed by a valid type and comma operator, not another label. For example, `.label1 .label2 ty` produces an error.
* Error Cursor appears on `.label1`
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
* Expecting a Type Got a Label


* A label cannot exist by itself, it is given meaning by having a type follow it. For example, `.label1 ` by itself produces an error.
* Error Cursor appears on `.label1`
* Message: Expecting a Type Got a Label


* Elements in the tuples need to be separated by commas, if they are not then this produces an error. For example, `.label1 ty .label2` produces an error.
* Error cursor appears on `.label2`
* Message: Expecting a type Got a label
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved

* Duplicate labels within a tuple are not valid, so they produce an error. The error will appear on the subsequent duplicate uses, not on the type as a whole. FOr example, the type `.label1 Num, .label1 Num, .label2 Num, .label1 Bool` will have errors on the second use of `.label1 Num` and `.label1 Bool`
* Error Cursor appears on second use of `.label1 Num` and `.label1 Bool`<br/>
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
* Expecting a Unique Label Got a Duplicate Label

# Labeled Tuple Expressions
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
<!-- TODO: add `.label` as a new expression form -->
Syntax: `.label1 e1, .label2 e2, ..., .labeln en`

Files to Edit: UHExp.re

To add labeled tuples, the operator type must be expanded to include the dot operator and operand type must be expanded to include labels.
```
type operator =
| Space
| Plus
| Minus
| Times
| FPlus
| FMinus
| FTimes
| LessThan
| GreaterThan
| Equals
| Comma
| Cons
| And
| Or
| Dot;
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
```
The Dot operator will be left associative and have highest precedence.
```
operand =
| EmptyHole(MetaVar.t)
| Var(ErrStatus.t, VarErrStatus.t, Var.t)
| IntLit(ErrStatus.t, string)
| FloatLit(ErrStatus.t, string)
| BoolLit(ErrStatus.t, bool)
| ListNil(ErrStatus.t)
| Lam(ErrStatus.t, UHPat.t, option(UHTyp.t), t)
| Inj(ErrStatus.t, InjSide.t, t)
| Case(ErrStatus.t, t, rules, option(UHTyp.t))
| Parenthesized(t)
| ApPalette(ErrStatus.t, PaletteName.t, SerializedModel.t, splice_info)
| Label(t)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

t is an expression, but label argument is a label (see types section above)

```
<!-- TODO: similar considerations as above -->

Partially labeled product expressions are allowed, and labels and non-labeled positions can be interleaved.
For example, the labeled product expression `(.x 2, 3, .y True)` is allowed.

Singleton label product expressions are supported. For example, `.x 2` is supported.

<!-- TODO: can you omit labels by providing values in order: `(1, 2, 3) <= (.x Num, .y Num, .z Num)` -->
An unlabeld product expression can analyze to a labeled product expression, allowing you to omit labels. For example, `(1, 2, 3) <= (.x Num, .y Num, .z Num)` is valid and each value in `(1,2,3)`. This operation happens positionally, and does not assign labels based on variable name if variables are used. For example, `(y, x, z) <= (.x Num, .y Num, .z Num)` is valid.

<!--
TODO: "Record punning" in Reason: `{x, y, z} => {x: x, y: y, z: z}` -- is there anything analogous that we can do? Does this interact with positional values? `(y, x, z) <= (.x Num, .y Num, .z Num)` does that operate positionally or via punning?
TODO: partially labeled values, where some of the arguments are in order: `(1, 2, .z 3) <= (.x Num, .y Num, .z Num)`. what about interleaving vs. requiring all the explicit labels at the end ala Python?
TODO: what are the type synthesis and type analysis rules for the labeled tuple expressions -->
### Punning
Some languages, such as Reason, have record punning. This is where a record's labels can be implied when it is declared using variables. For example, `{x, y, z} => {x: x, y: y, z: z}` is true. Similar punning fuctionality could be implemented in Hazel. For example, if this punnign was implemented `(x, y, z) => (x: x, y: y, z: z)` would hold true. However, this creates a question of if every tuple created with variables should be a labeled tuple. Given this additional complexity and added development costs, I believe that labeled tuple punning should be considered out of scope for the inital addition of labeled tuples.

### Projection Expressions
Labels can be used to access elements of a pair through projection expressions.
<!-- TODO: add `e.label` as a new expression form -->
`e.label` will be the new expression form. It will use the dot operator, which was already added to the operator type above. `e.label` expects `e` to be a labeled tuple type and `label` to match one of the labels within `e`. `e.label` will retun the value that has the label `label`.
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
#### Backspace
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

separate section on Action Semantics

You press backspace on `e |.label` and get to `e.label`

You press space on `e|.label` and get to `e .label`

### Type Sythesis and Type Analysis Rules for Labeled Product Expressions
#### Synthesis
![Syntheis Rule for Labeled Product](syn_2.png)
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved

![Synthesis Rule for Projection](syn_1.png)
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved

#### Analysis
![Analysis Rule Right](ana_1.png)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  • these two rules are for single tuple elements, but we also need a rule for n-ary labeled tuples that calls into this judgement.
  • e_1 should be analyzed against tau_1 (we know the expected type, so it is not necessary to synthesize). same with the second rule below.


![Analysis Rule Left](ana_2.png)
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved

### Expression Syntax Errors
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved

+ A label must be followed by a valid expression and comma operator, not another label. For example, `.label1 .label2 e` produces an error.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

see comments above on types

+ Proposed Error Message: Error Cursor appears on `.label1`
+ Message: Expecting an Expression Got a Label

+ A label cannot exist by itself, it is given meaning by having an expression follow it. For example, `.label1 ` by itself produces an error.
+ Error Cursor appears on `.label1`<br/>
+ Message: Expecting an Expression Got a Label

+ Elements in the tuples need to be separated by commas, if they are not then this produces an error. For example, `.label1 e1 .label2` produces an error.
+ Error cursor appears on `.label2`<br/>
+ Message: Expecting an Expression Got a Label

+ Duplicate labels within a tuple are not valid, so they produce an error. The error will appear on the subsequent duplicate uses, not on the type as a whole. FOr example, the expression `.label1 1, .label1 3, .label2 4, .label1 True` will have errors on `.label1 3` and `.label1 True`
+ Error cursor appears on `.label1 3` and `.label1 True`<br/>
+ Message: Expecting an Unique Label Got a Duplicate Label

+ Using the dot opearator as a binary operator on a type that is not a labeled tuple will produce an error. This error will appear on the expression to the left of the dot operator that is not a labeled product. For example, the expression `1.label1` will have an error on `1`.
+ Error currsor appears on expression to the left of the dot operator
+ Message: Expecting a labeled product Got a (type of expression in error cursor)

# Labeled Tuple Patterns
Syntax: `.label1 p1, .label2 p2, ..., .labeln pn`

Files to Edit: UHPat.re

To add labeled tuples, the operator type must be expanded to include the dot operator and operand type must be expanded to include labels.
```
type operator =
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
| Comma
| Space
| Dot;
```
The Dot operator will be left associative and have highest precedence.
```
and operand =
| EmptyHole(MetaVar.t)
| Wild(ErrStatus.t)
| Var(ErrStatus.t, VarErrStatus.t, Var.t)
| IntLit(ErrStatus.t, string)
| FloatLit(ErrStatus.t, string)
| BoolLit(ErrStatus.t, bool)
| ListNil(ErrStatus.t)
| Parenthesized(t)
| Inj(ErrStatus.t, InjSide.t, t);
| Label(ErrStatus.t, string)
ecdeuts marked this conversation as resolved.
Show resolved Hide resolved
```
<!-- TODO: similar considerations to labeled tuple expressions -->
Partially labeled product patterns are allowed, and labels and non-labeled positions can be interleaved.
For example, the labeled product type `(.x pat1, pat2, .y pat3)` is allowed.

Singleton label products are supported. For example, `.x pat1` is supported.

### Sythesis and Analysis
<!-- TODO: can you omit labels by providing values in order: `(1, 2, 3) <= (.x Num, .y Num, .z Num)` -->
An unlabeled product pattern can match to a labeled product expression, allowing you to ommit labels. For example, `(.x 1, .y 2, .z 3)` can match on the pattern `(a, b, c)`. This operation happens positionally.

A labeled tuple pattern must match the label names and the order of a labeled tuple expression for a pattern match. For example, `(.x a, .y b, .z c)` will match with `(.x 1, .y 2, .z 3)` but will not match with `(.y 1, .z 2, .x 3)` because the order does not match.

A partially labled pattern can match with a fully labled expression as long as the labels that do exist match. For example, `(.x 1, .y 2, .z 3)` will match on `(.x p1, p2, .z p3)`

### Punning
Punning may be useful for labeled tuple patterns, where the label can be used to access the element rather than adding an aditional variable. For example, with punning this code snippit:

```
let f = fun(.x, .y)
...
f(.x 1, .y 2)
```

would be equivalent to

```
let f = fun(.x x, .y y)
...
f(.x 1, .y 2)
```

This would be a great quality of life improvement to patterns with labeled tuples, and will be attempeted with the initial impelemntation of labeled tuples. It will be considered lower priority, since it is not required for labeled tuples patterns to function at a basic level.

### Pattern Syntax Errors

+ Multiple label must be followed by the comma operator, not another label. For example, `.label1 .label2` produces an error.<br/>
+ Error cursor appears on `.label 2`
+ Message: Expecting a Pattern Got a Label

+ Elements in the tuples need to be separated by commas, if they are not then this produces an error. For example, `.label1 p1 .label2 p2` produces an error. <br/>
+ Error cursor appears on `.label2`<br/>
+ Message: Expecting a Pattern Got a Label

+ Duplicate labels within a tuple are not valid, so they produce an error. The error will appear on the subsequent duplicate uses, not on the type as a whole. For example, the expression `.label1 p1, .label1 p2, .label2 p3, .label1 p4` will have errors on `.label1 p2` and `.label1 p4`
+ Error cursor appears on `.label2`<br/>
+ Message: Expecting a Unique Label Got a Duplicate Label

# What about records?
Records in other languages are very similar to the labeled tuples in this propoasal. Records are typically a data structure that bundles data together with labels and values, and the values are accessed using projection with the labels. The values are unordered in a record, while the values are ordered in a labeled tuple. A labeled tuple is able to perform the same functions as a record, while adding additional functionality by ordering data. If labeled tuples are sucessfully added to Hazel, then records will be redundant in Hazel.

# Appendix: Other Ideas
While creating this proposal, I considered many other ideas for Hazel labels. These ideas are detailed below.

### Reason like ~label annotations
Types: `~label1: ty1, ~label2: ty2,..., ~labeln: tyn`

Expressions: `~label1: ty1, ~label2: ty2, ..., ~labeln: tyn`

Patterns: `~label: ty1, ~label: ty2,..., ~labeln: tyn`

This was very similar to the final dot notation used. However, the dot opearator was chosen over the tilda operator since the tilda key is harder to acces than the dot on a keyboard, and the dot operator was already associated with projection so it made sense to associate it with label annotations as well.

### Space Separator with No Label Annotations
Types: `label1 ty1, label2 ty2, ..., labeln tyn`

Expressions: `label1 e1, label2: e2, ..., labeln: en`

Patterns: `label1 p1, label2 p2, ..., labeln pn`

This suggestion reduces the amount of additional operators needed for labled products. However, there is no way to tell distinction between undefined function variable application and labeled expression, so this syntax would not work.

### Colon Operator
Types: `label1: ty1, label2: ty2, ..., labeln: tyn`

Expressions: `label1: e1, label2: e2, ..., labeln: en`

Patterns: `label1: p1, label2: p2, ..., labeln: pn`

This syntax imitates many other languages, which use a colon operator to separate labels and values in record types. However, this creates onfusion between labeled pair type annotation and type annotations as they both would use the colon operator. For this reason, this option was not used.

### Colons and Braces
Types: `{label1: ty1, label2:ty2, ..., labeln:tyn}`

Expressions: `{label1: e1, label2:e2, ..., labeln:e2}`

Patterns: `{label1: p1, label2: p2, ..., labeln: pn}`

This syntax is more typical for a record, and may create confusion about labeled tuples as a value and records as a type definition. In addition, adding logic for braces within Hazel would increase implementation complexity a great deal.
Binary file added 1-labeled-tuples/ana_1.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added 1-labeled-tuples/ana_2.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added 1-labeled-tuples/syn_1.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added 1-labeled-tuples/syn_2.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.