PistonDevelopers/dyon

Add `#ERROR <string>` refinement type

bvssvni opened this issue · 2 comments

Related to #636

Sometimes you want to express that a function call will not work for some type.
You also might want to display a custom error message.

fn foo(a) -> {return a - b}
(str) -> #ERROR "This function does not work with `str`"

The #ERROR <string> refinement type corresponds to a void type, but with slightly different semantics.

Dyon does not use void explicitly anywhere, so I do not want to introduce it here. The void keyword would imply that the function does not return for e.g. str, but that is not true. You can still call foo by anonymizing the argument to any.

I want the semantics to be that an error gets reported if the type is refined.

One can also use this with any to close the world of refinement types for a function:

fn foo(a) -> {return a - b}
(f64) -> f64
(vec4) -> vec4
(any) -> #ERROR "This function does not work with this type"

From this information, the type checker can infer that if the output type is f64, the argument type must be f64. If the output type is vec4, the argument type must be vec4. This permits type refinement to propagate from output to input.