fir-lang / fir

MIT License
23 stars 3 forks source link

Error handling plan #11

Open osa1 opened 2 months ago

osa1 commented 2 months ago

(Original post in https://gist.github.com/osa1/38fd51abe5247462eddb7d014f320cd2)

Fir should have convenient handling of error values, using polymorphic variants.

Fir won't have subtyping for named types, but if necessary (and can be done while maintaining soundness) we can have subtyping for records and variants.

The type system should support these use cases:

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

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

fn f2(): Result[{`E1, `E2}, ()] =
    if x():
        Result.Err(`E1)
    else:
        Result.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():
        Result.Err(`E1): Result.Ok(())
        Result.Err(other): Result.Err(other) # other has type {`E2, `E3}
        Result.Ok(()): Result.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():
        Result.Err(`E1): Result.Ok(())
        Result.Err(other): Result.Err(other)
        Result.Ok(()): Result.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()
    Result.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:

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

osa1 commented 3 weeks ago

The PhD thesis "Type Safe Extensible Programming" describes a similar system where exception handling is represented using row types in function types.

Section 3.1.3 "Exception handlers as extensible cases" gives a few examples of what their type system accepts.

However it doesn't give examples of function subtyping examples above, so I'm not sure if the type system supports it. The examples it gives: