The Sirius Type System

Low-Friction Refinement
Basics
Systems and Constraints
Array Programming
Caveats

Low-Friction Refinement

A type system featuring refinement types can enforce properties of programs at compile time that are usually enforced with runtime errors. For example, if a type system tracks the possible values of integers, it could:

Detect potential overflows and divisions by zero
Check that array accesses are in-bounds
Enforce constraints on array shapes, such as the dimension requirements for matrix multiplication: C = AB implies for A[X, Y] and B[Y, Z], C[X, Z]

Full-fledged refinement types can go much further; for instance, they can statically verify security policies of a web application.

To realize these advantages, programmers of refinement-typed languages must specify the properties they want as types and write procedures that provably adhere to those types. For programmers in fields without critical correctness requirements, this may be a prohibitive amount of work.^{Dependent type systems are even more expressive than refinement alone, since verification need not be performed by an SMT solver. On the other hand, programming is hard, compiling is slow, and compiler errors for arithmetic constraint violations in particular can be "daunting in size."} The expressive power of refinement depends on the theories supported by the attending solver. Languages that support refinement, like Liquid Haskell, also often have other powerful type features.

Sirius instead only provides a single theory, polynomial integer arithmetic^{Unfortunately incomplete, courtesy of work on Hilbert's 10th problem.}, and an otherwise simple type system. We seek to limit expressiveness so that the types that can be expressed have extra syntactic and semantic support.^{A composer might limit themselves to a proven formula like the fugue or sonata for analogous reasons. The perfect tool to communicate a given idea has all expressiveness necessary and no more.}

The typechecker automatically tracks all integer values in the program as multivariate integer polynomial Polys on a best-effort basis. The choice of polynomial representation may seem arbitrary — this document will hopefully illustrate that it suits many use cases for array programming.^{One motivation to pique interest: polynomials are closed under addition and multiplication, the two operations needed to index a multidimensional array. Suppose we are given an array A[M, N, N] of square matrices. If we want the 2nd element of the 2nd row of the 3rd matrix, we compute A[2*N^2 + N + 1] (of course, usually written A[2, 1, 1]).} Encoding array sizes and accesses with Polys also unlocks potential optimizations for high-level array code.

Basics

The Sirius type system has a fundamental law: no type information may flow between functions except through their signatures. In other words, the typechecker performs inference only within function boundaries.

Sirius currently supports a small set of primitive types: boolean bool, 64-bit integer i64, and 64-bit floating point f64. We can combine types as tuples or functions.

fn main():
    let a = true             // bool
    let b = 1                // i64
    let c = 0.1              // f64
    let d = example          // function f64->bool
    let e = (a, (c, d))      // tuple (bool, (f64, f64->bool))
    let f: bool = example(c) // annotations are optional inside functions

// but mandatory for function signatures
fn example(x: f64) -> bool:
    return x > 3

Type parameters may be added to functions, but all expressions must have concrete types.

// the type parameter list is enclosed by curly brackets 
fn double{T}(x: T) -> (T, T):
    return (x, x)

fn main():
    print double(1)
    print double{bool}(true) // as are type parameters in expressions
    print double(double{f64})

Sirius tries to track all integer values as polynomials. This means we can perform arithmetic in the type system, but as soon as a value cannnot be represented as a polynomial (for instance, if it is the result of an arbitrary function call or division without an exact result), it must be given a fresh type variable.

// this function returns a plain i64
fn untracked() -> i64:
    return 100

fn main():
    let x = 1                 // i64(poly = 1)    
    let y = untracked()       // i64(poly = 'a)
    let z = x + y             // i64(poly = 'a + 1)
    let w = (y^2 - 9)/(y + 3) // i64(poly = 'a - 3)

We cannot perform value inference with mutable integers.^{Well, we could try, but it doesn't play nicely with control flow.} Iterators are considered immutable for type purposes.

fn main():
    let mut x = 0       // plain i64
    for i from 0 to 10: // i64(poly = 'a)
        x = x + i

Integer literals are legal types, representing constant polynomials. Poly variable names cannot be spelled in general.

fn get_two() -> 2:
    return 2

fn main():
    let a: 3 = 3
    let b: 5 = a + get_two()

This diagram illlustrates the possible promotion and demotion paths of integer values in a Sirius program. Promotions always create a new equation, as described in the next section.

Systems and Constraints

To express non-trivial refinements, we must allow Poly type variables in function arguments. When the Sirius typechecker unifies two Polys at a function call or return statement, it creates an equation.

The Sirius Type System

Low-Friction Refinement

Basics

Systems and Constraints

Array Programming

Caveats