RFC 001: Extend Quint type system to support Sum Types #1062

shonfeder · 2023-07-19T20:20:07Z

This RFC proposes the design for sum types to be introduced to quint.

The overview gives the gist of the proposal and detailed discussion follows.

Closes #673.

Tests added for any new code
Documentation added for any new functionality
Entries added to the respective CHANGELOG.md for any new functionality
Feature table on README.md updated for any listed functionality

doc/rfc001-sum-types.md

konnov

This is very detailed RFC. Thank you for thinking about the sum types. I reviewed this document with the VSCode plugin, so this may have lead to too many comments. If it's too hard to read on Github, try the plugin.

doc/rfc001-sum-types.md

konnov · 2023-07-20T12:38:00Z

doc/rfc001-sum-types.md

+In the presence of row-polymorphis, however, the responsibility of the recipient
+is relaxed: the recipient can just handle a subset of the possible alternatives,
+and if the expression falls under a label they are not prepared to handle, they
+can pass the remaining responsibility on to another handler.


This explanation makes sense to me. However, I am not sure how we would handle that in Apalache. Maybe it is not a problem at all, since Apalache variants would require us to write series of IF-THEN-ELSE with unsafe access, but we should check that.

We can translate this into Apalache IR using the VariantGetUnsafe and VariantTag operators, like the pattern here:

https://github.com/informalsystems/apalache/blob/4e0094ee5d03a068188a85dcdc8ead021b17033e/src/tla/Option.tla#L34-L60

doc/rfc001-sum-types.md

shonfeder · 2023-07-21T08:06:38Z

I still need to do a pretty extensive editing, clean up, and revision pass, but I've made the following improvements following our conversation:

Committed a generated pdf, so the latex is easily and reliably readable. Feedback as annotated PDF is welcome!
Made the syntax more rust-like in the ways we discussed (swapped | for ,)
Added a fragment from the ERC20 spec that has been adapted to use sum types, so we can get a feel for what this syntax will look like in a spec.
Changed the injection rule so that we ensure a (necessarily closed) sum type has been defined.
Some cleanup to the first part of the doc.

Sorry for the rough state of the rest, but I look forward to any thoughts in these changes. How do you feel about this syntax?

konnov

I left a few comments to the new version. Thank you for producing a pdf. It's way easier to read!

konnov · 2023-07-21T15:24:49Z

doc/rfc001-erc-sum-types-example.qnt

+    pure def flatMap(r:Erc20Result, f:Erc20State => Erc20Result): Erc20Result = r match {
+         Ok(s)    => f(s),
+         Error(_) => r
+    }


can we not call it flatMap? We want a friendly specification language :)

Maybe “niceMap”? Lol 😂

konnov · 2023-07-21T15:32:37Z

doc/rfc001-erc-sum-types-example.qnt

+
+    // Example of a sum type representing a
+    // NOTE: Once we support parametric sum-types we can generalize this alias and the map operators
+    type Erc20Result = {


I really like it. But now I can see that we might want to introduce enum and struct at some point to disambiguate the types. We could make these keywords optional. Syntactically, the types are still different, but it may be a bit too hard to spot the difference without a helper keyword.

Yeah, that is really the worry I have too. I think the | is really a nice option. Again, people in type script don’t seem to have any problem with it.

Having optional keywords is not a good idea imo: it means inconsistent code for readers and unnecessary variance on trivial things. If we must add keywords, let’s please make them required?

To help us get a clear and holistic vision of how all the bits of syntax fit together in our (and other) languages, I'll put together a table comparing the different constructs in different languages.

I am worried that if we try to over-index on superficial similarity to rust one corner of the language, we will lose the bigger picture, and its import all our syntax works together. Rust's syntax for sum types makes particular decisions in light of other aspects of the syntax, many of which we don't share. So, imo, we should make sure if adopt rust-isms that they fit with the rest of our syntax, or that we make needed adjustments to rustify other aspects of our language too.

In discussion with the team last week, all three of us agreed that the | based syntax seemed most sensible given the rest of our syntax. I've expanded the RFC to discuss the trade offs in some depth, and I've outlined some considerations on how we could change our syntax if we want to pursue a more rust-like syntax.

For the short term, I've moved forward with | for the concrete syntax, but we are not considering it stable at all at this point.

doc/rfc001-erc-sum-types-example.qnt

konnov · 2023-07-21T15:58:32Z

doc/rfc001-sum-types.org

+pure def A(x:int): T = variant("A", x)
+pure def B(x:str): T = variant("B", x)
+pure def C(): T      = variant("C", {})


Do we want to generate A, B, C, or T::A, T::B, T::C (similar to rust)? If we strive for minimality, probably the former

The latter would conflict with our module system notation: it would not be clear from syntax whether you were accessing a module operator.

If we supported nested modules, we could generate a module with operators for the constructors, but we don’t support that. So I don’t know how we could resolve that ambiguity. I also don’t see the benefit for practically to that syntax Do you have anything in mind?

Afaict, Rust doesn’t have that ambiguity because their modules names must be lower case. function names must also be lower case, upper case is reserved for types and data constructors.

My only worry is that enums tend to produce conflicts. This is probably why languages like Java hide the individual constants under the enum's namespace. I guess, Rust does something similar. Sure, it's not an issue, if the spec write introduces unique names.

Co-authored-by: Igor Konnov <[email protected]>

Also filled in some of the discussion around why we'll eschew row-polymorphic sum types and considerations re: Rust's syntax.

GitHub recognizes the `$$` demarcater for latex, but not the `\[` that was being used. Should improve readability!

- Use `|` - Detail issues with naive adoption of Rust's syntax - Fix some syntax

konnov

I read the syntax part in detail and skimmed through the detailed part, as I have read it before. I agree with the syntax. Let's start with this one. We can always change the grammar later. I actually did not know that Quint admits empty records: {} does not parse as a record, but Rec() does. If we want to rely on Rec() being the unit value/type, we have to emphasise this decision in the language document.

shonfeder · 2023-08-21T15:26:32Z

If we want to rely on Rec() being the unit value/type, we have to emphasise this decision in the language document.

With the current design this isn't user-facing, and we don't have to rely on this, we could always switch to a different canonical unit. But the empty record works for now, since it will always be isopmorphic to the unit! :)

Maybe we can add this to lant.md and adjust the syntax to support it if we end up funding it ergonomic enough. WDYT?

shonfeder · 2023-08-21T15:27:00Z

Thanks for the review!

shonfeder force-pushed the 244/sum-types-design branch from 81fa66c to 01b0c2e Compare July 19, 2023 20:27

shonfeder requested a review from konnov July 20, 2023 03:43