Dyon is a rusty dynamically typed scripting language.

What are simple refinement types?

A simple refinement type system is an "extra layer" of types in addition to the normal type signature of functions. This is used to catch more errors before runtime.

The extra layer contains special knowledge about the function or alternative semantics from how the function is used.

Dyon supports ad-hoc types which lets you write e.g. Unknown bool instead of just bool. Simple refinement types in Dyon works seamlessly ad-hoc types.

For example, one can use this to type check many-valued boolean logic:

use std as std

fn flip() -> Unknown bool {return if random() < 0.5 {false} else {true}}
fn tr() -> True bool {return true}
fn fa() -> False bool {return false}

// Override `!` operator.
fn not(a: bool) -> bool {return std::not(a)}
    // Use simple refinement types to add extra type information.
    (True bool) -> False bool
    (False bool) -> True bool
    (Unknown bool) -> Unknown bool

fn check_tr(_: True bool) {}

fn main() {
    a := flip()
    check_tr(!a)
}

The ad-hoc type Unknown bool is constructed by a coin-flip. If you invert a coin-flip, you don't know whether it is true or false, so it is still Unknown bool.

Dyon detects an error in the code above:

Type mismatch (#100):
Expected `True bool`, found `Unknown bool`
17,14:     check_tr(!a)
17,14:              ^

In this example, I used simple refinement types to reason about nondeterministic behavior of many-valued boolean logic. Instead of writing code explicitly as many-valued boolean logic, one can use ad-hoc types to lift the many-value logic to type level.

Design

For design, see #636

This PR adds support for simple refinement types in Dyon. This allows e.g. binary operators to be type checked as external functions.

• Moved all unary and binary operations from runtime to the standard library (see Move binary and unary operators to external functions #635)
• Make std namespace for standard external functions (see Make namespace std for standard external functions #639)
• Added lots of tests for type refinement
• Added support for ad-hoc variables in refinement types (see Add support for ad-hoc variables in refinement types #645)
• Added support for lazy invariants (see Lazy invariant following argument type #640)
• Added check__in_string_imports (type checker knowledge, see Add check__in_string_imports #646)
• Added lazy invariant for unwrap_or

Improvements in performance

There is a 4.4% improvement in performance on the n-body benchmark for n=100_000. This is a longer run that is tested manually and measures performance on typical game-logic workloads.