Sum types?

[Kmeakin]

Fathom currently has anonymous product types (records), but no (convenient) way of expressing sum types.

Potential solutions

• Do nothing. Encode sum types as dependent records (eg let Option : Type -> Type = fun T => {tag : Bool, value : if tag then T else {})
• Anonymous sum types, dual to records: (eg let Option : Type -> Type = fun T => sum {None : {}, Some : T})
• Algebraic data types a la Haskell, ML, Rust etc
• Polymorphic variants

Design considerations

• Are they ergonomic to use?
• Can they express recursion?
• Can they be compiled efficiently?
• Nominal or structural?
• Row polymorphism?
• First class labels?

Prior Art

• (Generalized) Algebraic data types: Haskell, Agda, Coq, Idris, Ocaml
• Anonymous sum types: Haskell, Dhall
• Polymorphic variants: Ocaml

[eashanhatti]

Another consideration is recursive types! If sum types are not anonymous then things become a lot easier, but if they're anonymous it gets tricky. In the latter case, maybe you could use isorecursive types and insert roll and unroll during elaboration?

[brendanzab]

At one stage I was thinking you could add an structural enum type:

enum { l₁, ..., lₙ } : Type

       lₘ ∈ { l₁, ..., lₙ }
────────────────────────────────
 enum lₘ : enum { l₁, ..., lₙ } 

  e : enum { l₁, ..., lₙ }      t₁ : t  ...  t₁ : tₙ
─────────────────────────────────────────────────────
  match e { enum l₁ => t₁, ..., enum lₙ => tₙ } : t

Which could be used for the tags of records. This is a bit like Martin Löf’s finite sets (I think?). I was also thinking that there would be some corresponding format for enums as well. In this case we’d need some syntactic sugar or elaborator support to make tagged unions bearable if we went that route. I’d also imagine that it would require us to implement dependent pattern matching on records (which we don’t yet do). And yeah recursive types, and mutually recursive types could be… fun?

We already have top level items so maybe it would be easier to go with top level tagged union declarations like Haskell, OCaml, Rust? Save the experimentation for another time and place?

[brendanzab]

IIRC Mini-TT had some simple form of tagged union that might be interesting to look at.

[brendanzab]

I think one thing that might help in terms of design is thinking in terms of how this might help us with binary data descriptions. Eg. Looking through the OpenType data description, where would tagged/disjoint unions help us. And also make us think about how we might have corresponding formats that might produce these tagged unions.