Simple refinement types following function declaration

[bvssvni]

This is a feature that might help with https://github.com/PistonDevelopers/dyon/issues/635

A simple refinement type in Dyon is extra type information than can be added after function declaration to catch more errors with the type checker.

For example:

fn add(a: any, b: any) -> any {return a + b}
    (f64, f64) -> f64
    (vec4, f64) -> vec4
    (f64, vec4) -> vec4
    (vec4, vec4) -> vec4
    (mat4, mat4) -> mat4
    (str, str) -> str

The extra type information is only used by the type checker and can be otherwise ignored.

Another example:

// Use `any` implicitly.
fn foo(x) -> {return x + 1}
    // Add simple refinement types to catch more errors.
    (f64) -> f64
    (vec4) -> vec4

bar(x: f64) = x + 1

fn main() {
    x := bar(foo((1, 2))) // ERROR: Expected `f64`, found `vec4`
    println(x)
}

The type checker understand that since (1, 2) is vec4, the return type will be vec4, which collides with the expected argument type f64:

 --- ERROR --- 
In `source/test.dyon`:

Type mismatch (#100):
Expected `f64`, found `vec4`
10,14:     x := bar(foo((1, 2)))
10,14:              ^

Ignorance of code

The type checker does not check whether refinement types are correct according to the code inside the function body. It only checks whether refinement types are sub-types of the default type signature.

This design is because code written in Dyon is almost always faster when translated into Rust, so the language is designed to be used that way. External functions are "black boxes" for the type checker and therefore it must trust the function signature and extra type information anyway.

If you call functions with refinement types inside a new function, this information does not propagate automatically:

fn foo(a: any) -> any { ... }
    (f64) -> f64
    (vec4) -> vec4

fn bar(a: any) -> any { return foo(a) }

fn main() {
    println(bar("hi")) // Type checker does not know that `foo` is called by `bar`
}

To expose refinement types, extra type information must be added:

fn foo(a: any) -> any { ... }
    (f64) -> f64
    (vec4) -> vec4

fn bar(a: any) -> any { return foo(a) }
    // Teach type checker what happens in `bar`
    (f64) -> f64
    (vec4) -> vec4

fn main() {
    println(bar("hi")) // Type checker does not know that `foo` is called by `bar`
}

Ambiguity checking

Refinement types are read from top to bottom by the type checker. At each step, the type checker checks for ambiguity before deciding to proceed.

Ambiguity means that if the type checker infers more about the code, it might figure out that the types matches or that they fail, but at this point in time, the type checker can not tell the difference. Instead of proceeding to the next line, the type checker decides to wait until it has learned more.

Ad-hoc types require ambiguity handling when refining the type of a function call, but are otherwise well-behaved for simple refinement types because they do not trigger premature type errors.

Closed world assumption

The type checker assumes that if the type of the arguments do not match any of refined types (without ambiguity), an error should be reported. This is called a "closed world assumption", meaning that it is not assumed that more type refinements might be added later. It assumes that the specified refinement types are all there is.