Skip to content

Instantly share code, notes, and snippets.

@osa1
Created June 30, 2024 11:35
Show Gist options
  • Save osa1/38fd51abe5247462eddb7d014f320cd2 to your computer and use it in GitHub Desktop.
Save osa1/38fd51abe5247462eddb7d014f320cd2 to your computer and use it in GitHub Desktop.
Anonymous polymorphic variant (sum) types design

Anonymous polymorphic variant (sum) types design

We need a type system that supports the use cases listed below.

Specifically I'm interested in making anonymous sums useful for error handling.

The syntax below are just an example. The final syntax will depend on the type system that will be used to support these use cases.

Also note that the language already has parametric polymorphism with constraints (i.e. typeclasses). The questions about subtyping vs. row poly. below are only for anonymous variants. Named types won't have subtyping.

The use cases:

type Result[E, T]:
    Err(E)
    Ok(T)

# Thrown errors should be reflected in the type.
fn f1(): Result[{`E1}, ()] =
    Err(`E1)

fn f2(): Result[{`E1, `E2}, ()] =
    if x():
        Err(`E1)
    else:
        Err(`E2)

# Type of a function can have more error variants than what the function
# actually throws. This can be useful to e.g. allow backwards compatible
# changes in the function.
fn f3(): Result[{`E1, `E2, `E3}, ()] = f2()

# Handled errors are not propagated.
fn f4(): Result[{`E2, `E3}, ()] =
    match f3():
        Err(`E1): Ok(())
        Err(other): Err(other) # other has type {`E2, `E3}
        Ok(()): Ok(())

# Higher-order functions propagate errors from function arguments.
# Here kind of `Errs` is `*`.
fn f5[Errs](f: Fn(): Err[Errs, ()]): Err[Errs, ()] =
    f()

# A combination of `f5` and `f4`.
#
# This is a bit more tricky than `f5`: `Errs` is a row type, not a `*`.
#
# Do we need a constraint here saying that `Errs` doesn't have `E1`?
fn f6[Errs](f: Fn(): Result[{`E1, ..Errs}, ()]): Result[{..Errs}, ()] =
    match f():
        Err(`E1): Ok(())
        Err(other): Err(other)
        Ok(()): Ok(())

# Question: can we express `f6` in a system with subtyping instead of row
# polymorphism?
#
# The return type would have to be more precise (with less number of variants)
# than the return type of `f`. I don't know how to express this without a type
# variable standing for a row.

# Similar to `f6`, but the call site adds more error cases.
#
# What if `Errs` is instantiated as a variant with `E1`?
#
# I think that's OK (i.e. sound), but the instantiated return type shouldn't
# have two `E1`s.
fn f7[Errs](f: Fn(): Result[{..Errs}, ()]): Result[{`E1, ..Errs}, ()] =
    f()
    Err(`E1)

# Function subtyping: a function that returns less can be passed as a function
# that returns more.
fn f8(f: Fn(): {`E1, `E2}) = ...

fn f9(): {`E1} = ...

f8(f9)          # This should type check.

# Function subtyping: a function that expects more can be passed as a function
# that expects less.
fn f10(f: Fn({`E1, `E2})) = ...

fn f11(a: {`E1, `E2, `E3}) = ...

f10(f11)        # This should type check.

Questions:

  • Can you think of any other use cases that the type system should support, to make error handling via anonymous variants convenient and expressive?

    Note: I'm not asking about syntax features. We can make it less verbose/nicer once we have a type system that is expressive enough.

  • Can f6 be expressed in a system with subtyping instead of row polymorphism? How?

  • Can function subtyping examples work in a system with row polymorphism? How?

  • Assuming both are possible, what do I win/lose by chosing one or the other?

Note: the choice of row poly. or subtyping will only apply to anonymous variants and records. The language already has parametric poly. with constraints/bounds (i.e. typeclasses) and won't have subtyping for named types.

@osa1
Copy link
Author

osa1 commented Sep 22, 2024

A relevant paper: Restrictable Variants: A Simple and Practical Alternative to Extensible Variants
(https://drops.dagstuhl.de/storage/00lipics/lipics-vol263-ecoop2023/LIPIcs.ECOOP.2023.17/LIPIcs.ECOOP.2023.17.pdf)

@osa1
Copy link
Author

osa1 commented Dec 31, 2024

The function subtyping cases above can be implemented with the right placement of row variables: https://github.com/fir-lang/fir/blob/9ec9d261f5c8fda98acf43d99317a5b7395df82b/tests/Rows3.fir#L49-L64

For better ergonomics, the row variables can be hidden by marking extensible variants somehow. I think OCaml takes this approach with the [> ...] and [< ...] syntax.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment