tact-lang / tact

Tact compiler main repository
https://tact-lang.org
MIT License
267 stars 53 forks source link

Support for `Either` type in tact #379

Open 0kenx opened 1 week ago

0kenx commented 1 week ago

Tact should add support for Either TL-B type.

I propose we use the ? operator: TL-B Either X Y -> Tact X ? Y. If it's too confusing we could also use a more explicit syntax Either<X, Y>.

anton-trunov commented 1 week ago

Yes, this is needed to implement #322. I'd propose to use the pipe symbol | instead of ? because it's essentially a type analogue of logical disjunction and there won't be grammar conflicts with the optional type operator: https://github.com/tact-lang/tact/blob/da6a7f6e3eb56a20f5daafa84e50d095f923f3ba/src/grammar/grammar.ohm#L24.

We should also outline the concrete syntax for the constructors and destructors for the Either type.

To construct an expression of an Either type, we need two constructors, we can reuse the Left and Right names that TL-B borrows from Haskell, because it's more general than what, for instance, Rust does with Ok and Error.

To destruct an expression of an Either type, we need pattern-matching:

let foo: X | Y = ...;
match foo {
  Left(l) => {
    return 42;
  }
  Right(r) => {
    return 24;
  }
}

or, in Ohm.js-like notation:

StatementMatch ::= "match" Expression "{" ListOf<MatchClause, ","> ","? "}"

MatchClause ::= Pattern "=>" "{" Statement* "}"

// patterns can be nested
Pattern ::= Constructor ("(" NonemptyListOf<Pattern,","> ","? ")")?
        | TactIdentifier
        | "_"

...

This could be good enough for an initial implementation, later we could support things like | for grouping patterns, etc. The initial implementation does not have to support the general algebraic data types, just the Either type.

0kenx commented 1 week ago

The only problem I have with using | is that, in many languages with sum types, | is either straight away commutative, or implementation details are hidden well enough so developers can treat it as commutative.

TL-B on the other hand, makes a clear distinction with the selector bit. And because we want Tact code to interoperate with TL-B definitions, there's no way to abstract that implementation detail away.

anton-trunov commented 1 week ago

Well, because it is commutative. In the sense that you can always build an isomorphism between Either X Y and Either Y X.

0kenx commented 1 week ago

Yup, but serializing type X in Either X Y would result in 0b0xxxxxxxx, and serializing X in Either Y X would result in 0b1xxxxxxxx. If people take the type from FunC and change the order without realizing what is under the hood it would lead to errors.

anton-trunov commented 1 week ago

Yeah, that's a good point, but still more verbose syntax won't prevent this. I'm happy to change my opinion if you have a convincing concrete example, though

novusnota commented 1 week ago

We may come up with an or keyword (as in Either ... or ...). It won't describe the layout, but it also won't be confused with general ADTs (not nearly as much as | would).

let foo: X or Y = ...;

As a bonus it pairs nicely with as serialization modifier, introducing a stronger visual bond between left and right parts as opposed to | or comma in Either<..., ...>

More examples:

// Maybe of Eithers'
let foo: (X or Y)? = ...;

// Alternative Maybe of Eithers'
let foo2: X or? Y = ...;

// Either of Maybes'
let bar: X? or Y? = ...;

// Throwing as into the mix
let baz: (X as uint64 or Y as coins)? = ...;
let baz2: X as uint64 or? Y as coins = ...; // alternative maybe of eithers'
Gusarich commented 1 week ago

// Alternative Maybe of Eithers' let foo2: X or? Y = ...;

@novusnota what’s that in TL-B notation?