[Relay] Add ADTs to text format

[weberlo]

This PR tackles some of item 0 from this issue, using this RFC as a reference.

One notable deviation is that match expressions can be specified as incomplete (i.e., not requiring all cases to be covered) by writing match?.

The tests in test_ir_parser.py currently do not pass if I don't inline every expression in the pretty printer. This is because when graph vars are created, scoping becomes more complicated. For example, the following program

def @length[A](%xs: List[A]) -> int32 {
match? (%xs) {
| Cons(_, %rest) => 1 + @length(%rest)
| Nil => 0
}
}

would be pretty-printed like so

def @length[A](%xs: List[A]) -> int32 {
%0 = 1 + @length(%rest)
match? (%xs) {
| Cons(_, %rest) => %0
| Nil => 0
}
}

. While this can still be parsed (by delaying evaluation of the graph expr until the context of its usage is available), it seems to add additional complexity without any benefits that I'm aware of. It also makes testing equality with the original program more difficult.

Hopefully, this brings us closer, if not all the way there, to writing Relay's prelude in the text format.

CC @jroesch@MarisaKirisame@joshpoll@slyubomirsky@junrushao1994

[slyubomirsky]

Thank you for adding tests for the additional features.

Higher-level point of discussion: What syntax do we want to settle on for text format type definitions? I like the style @weberlo used here (similar to OCaml's), but it may contrast a bit with other syntax we have (e.g., it doesn't use curly braces).

Also on the subject of syntax, I think it may be a little redundant to include the line separators | between match clauses when we use braces to delimit a match block and each pattern must match exactly one expression. Do we want braces around the expression in the match clauses? As in, pattern => { expr }? Since there can only be one expression, the braces might be redundant, though.

One reason I am raising these questions is so we can update our documentation to be consistent with the syntax we actually implement.

[weberlo]

@slyubomirsky I agree on the vertical bars in match exprs. I was originally just implementing the syntax from the RFC and hoping to reopen the discussion in this PR.

If we remove the bars from match, then it falls more in line with Rust syntax. We could then use Rustish syntax for ADT definitions. An example Rust enum is

enumWebEvent{// An `enum` may either be `unit-like`,PageLoad,PageUnload,// like tuple structs,KeyPress(char),Paste(String),}

and we could just replace enum with type.

We could also allow optional braces in match arms, which would be useful for sequencing.

match %ayy_lmao {
Ayy => 0
Lmao => {
@mutate();;
1
}
}

The last minor point is that if we're going with Rust syntax, should we also require commas after match arms?

[MarisaKirisame]

please extend graph_equal for this.

[MarisaKirisame]

also:maybe change the name of graph_equal to something better (freevars_eq e.x.)

[weberlo]

@MarisaKirisame Is there not a more standard PL name for the type of equality that graph_equal encodes?

[MarisaKirisame]

@weberlo alpha_equal_up_to_free_vars. unifiable is also good.

[MarisaKirisame]

Update the version number to 0.0.4.

[slyubomirsky]

On syntax, I like the idea of optional braces but we should be certain that this will not cause problems for round-tripping. I think commas in type definitions and match definitions in the Rust style might be good in that they more closely resemble C-like syntax

[weberlo]

@slyubomirsky@MarisaKirisame I took a crack at implementing Rust-style syntax in the most recent commits. Take a look when you get chance.

[MarisaKirisame]

why trailing comma?

[weberlo]

idk. it's not necessary. just a matter of style.

[weberlo]

I've just added support for external type declarations (example syntax is extern Type[A]), per @jroesch's suggestion. It will allow for importing opaque types which can be interacted with via operators.

[slyubomirsky]

Might be a good idea if we can avoid repeating ourselves, though are we certain that these definitions (something we will always inline and atomic expressions) will always coincide?

[weberlo]

Yeah. I was originally thinking it might be a good idea, but I'm not convinced they should be merged anymore.

[slyubomirsky]

Maybe we shouldn't include the syntax while we don't have the feature implemented (e.g., leave it for a different PR)

[weberlo]

@jroesch is planning on updating it very soon for the VM. He just wanted me to add all of the necessary boilerplate.

[slyubomirsky]

okay

[jroesch]

I need this change ASAP, I just want the parsing changes to be shipped in a unit to keep things clean.