Static types in SIL

Goals:

  • Document intentions and expectations
work(Duration dt, Coffee c) => Code: ...
  • Catch some mistakes early
xs |> fold(0, (a,b)=>a+b)
  • In future: run faster by doing less run time checks / branching
iota(1_000_000) |> map(x => x+1) |> sum

Principles

  • Start with looking at existing SIL code and see what we can reason about
  • Keep it simple, don't bring D complexity into SIL
long foo(const(char)[] a, immutable Thing b, short c = 55);   // D

foo : (string, Thing, int) -> int                             //SIL
  • Just enough features to describe SIL

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}
  • 2 : integer
  • 3.3 : number
  • true : boolean
  • "error" : string
  • foo : function must take 3 args and return boolean or string

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What's a.length?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What's a.length?

a = "Hello there"
a.length

String?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What's a.length?

a = [2,3,4]
a.length

Array?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What's a.length?

a = {"height":5, "length":8}
a.length

"table"?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What's a.length?

a : {"length":_, ...}

a is something with a field "length".

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is t?

t : {"day":_, "month":_, ...}

Something with fields "day" and "month".

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is b[c]?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is b[c]?

b = [3,4,5]
c = 1
b[c]    // 4

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is b[c]?

b = {"name": "Bob", "age": 34}
c = "name"
b[c]    // "Bob"

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is data[1 : $-1]?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is data[1 : $-1]?

data = [20,30,40,50,60]
data[1 : $-1]   // [30,40,50]

array

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is data[1 : $-1]?

data = iota(5)
data[1 : $-1]   // [1,2,3]

range

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is data[1 : $-1]?

data : [...]

data is a sequence of something

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is someFlag?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is someFlag?
A boolean.

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is d * 10?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is d * 10?
d must be numeric - either integer or number.

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is [d * 10, 'S', x]?

What types can we see looking at SIL code?

someFun(a,b,c) => {
    d = match( foo(a.length, 2, 3.3) ) {
         | true => b[c]
         | "error" => data[1 : $-1]
    }
    t = dates.today()
    x = if someFlag then t.day() else t.month()
    in [d * 10, 'S', x]
}

What is [d * 10, 'S', x]?
[numeric | char | whatever-x-is]

SIL types:

Basic types

integer a.k.a. int, number, char, boolean, void

Functions: (a,b,c) -> d

() -> boolean , (int, char) -> number

Sequences: [a]

[true,true,false] : [boolean], iota(1000) : [int]
[char] a.k.a. string

Union types: a | b

if b then 2 else "no" : int | string

SIL types:

Structs - former "tables", things with fields

{"name" : "Bob", "age" : 30} : {name : string, age : int}

Named structs and D objects:
Person {name : "Bob", age : 30} has the type Person {name : string, age : int}

> :st DivResult
DivResult {
  quotient : integer,
  remainder : integer
}

One dirty secret:

a = [1,2,3,4]
b = a.front
n = a.length

arrays & ranges have fields => they are also structs

{
  length : integer,
  front : #t,
  #elements: #t
}

Generics:

type Dated(T) = { val : T, date : dates.Date }

addDate(x) => { "val": x, "date": dates.today() }

> :st addDate
(#x x) -> Dated!(#x)
> addDate("hey")
:: Dated!(string)
{"val":"hey", "date":2021-Jun-15}

Generics:

type Result(V,E) = Yay { val : V } | Nay { err : E }

root(x) => Result!(number, string):
  if x >= 0 then Yay { "val": math.sqrt(x) }
            else Nay { "err": "root of a negative number" }

fmap : ( Result!(#a, #e), (#a) -> #b ) -> Result!(#b, #e)
fmap(r, f) => match(r) {
  | Yay {"val":x} => Yay {"val": f(x) }
  | Nay {...} => r
}

Overloading

D:

void write(int x);
void write(string s);
void write(string filename, string s);

SIL:

f(a) => { ... write(a); ... }

write : (int | string) -> void & (string, string) -> void

Using types in SIL code: variables

int a = 2
string s = xs |> map(text) |> _[0]
int | string ios = 44
boolean b = "true"

Call stack:
> (repl:1:13)
   ┌─ repl
 1 │ boolean b = "true"
   │             ^^^^^^ This might be string
 1 │ boolean b = "true"
   └ ^^^^^^^^ This should be boolean
Error: A value that might be string cannot be used where boolean is expected.

Using types in SIL code: functions

foo(int a, boolean b) => if b then a else a+1
foo(int a, b) => if b then a else a+1
greet(Person p) => print("Hi " ~ p.name)

(int x) => x+1                  // lambdas
(char a, char b) => [a,b,b,a]

// lambdas
x => int: x+1
(char a, char b) => string: [a,b,b,a]

//functions
foo(a, b) => int: if b then a else a+1
greet(Person p) => string: "Hi " ~ p.name

btw

> foo(a, b) => int: if b then a else a+1
> :st foo
(integer a, boolean b) -> integer

Using types in SIL code: matching on types

gimmeIntOrStr = match {
  | int x => x*10
  | string s => s.length
}

gimmeIntOrStr1 = match {
  | (int x) => x*10
  | (string s) => s.length
}

ntimes(str, cnt) => string:
  match(str, cnt) {
    | (string s, int n) when n > 0 => repeat(s, n) |> join
    | (string _, int _) => "cnt must be positive"
  }

Using types in SIL code: matching on types

Currently works only for basic types (int, number, boolean, char, and string) and names of registered D types.

> rem(a) => match(a) { | DivResult r => r.remainder }
> :st rem
(DivResult w) -> integer

Pattern matching happens at run time and uses the run time tags present in the value.

Using types in SIL code: casts

> json.parseJson("false") as boolean
:: boolean
false
> json.parseJson("false") as int
:: integer
Call stack:
> (repl:1:1)
Error: The value is described statically as integer but its runtime type is boolean.

> json.parseJson("33") as int
:: integer
33
> json.parseJson("33") as char
:: char
Call stack:
> (repl:1:1)
Error: The value is described statically as char but its runtime type is integer.

Using types in SIL code: type axioms

type Expr = int | Add { a : Expr, b : Expr }

f : (Expr) -> int
f(e) => match(e) {
  | int x => x
  | Add {"a":a, "b":b} => f(a) + f(b)
}

Here we annotate the type of f using an axiom to help SIL cope with a recursive type.

Subtyping

f(o) => o.x + o.y

> {"aa": "hey", "x":3, "z": false, "y": 4} |> f
:: integer
7

> g(x) => match(x) { | 1 => "a" | false => "b" }
> :st g
(boolean | integer x) -> string
> g(1)
:: string
"a"
> q => g("eh")
Call stack:
> (:1:1)
Error: Cannot use string where expected boolean | integer.

Subtyping

{x:int, y:int} <= {x:int}
{x:int, y:int} <= {y:int}
{x:int, y:int} <= {}

Coord {x:int, qq : char, y:int} <= Coord {x:int, y:int}
Coord {x:int, qq : char, y:int} <= {x:int, y:int}
Coord {x:int, y:int} <= {x:int, y:int}
but
Coord {x:int, qq : char, y:int} is not a subtype of Point {x:int, y:int}
and
{x:int, y:int} is not a subtype of Coord {x:int, y:int}.

Subtyping

Unions:

int <= (int | string)
(int | string) <= (int | boolean | string)

Functions:

If A2 <= A1 and R1 <= R2 then (A1) -> R1 <= (A2) -> R2.

Note the reversed order for argument types (they are contravariant).

Type checking & inference: how it works

toStr(x) => match(x) { | int n => text(n) | string s => s}
> :st toStr
(integer | string x) -> string

foo(o) => {
  a = o.fred |> toStr
  b = o.toto
  a = a.length
  in if b then a else o.fred + 2
}

Process one top level definition at a time:

  1. Walk the AST computing types and collecting constraints.
  2. Solve the constraints finding the type of the top level thing, report errors if constraints are inconsistent.

Type checking & inference: how it works

  1. Walk the AST computing types and collecting constraints.

Constants like 2 or true give obvious types. Expressions and newly defined variables give fresh type variables (a.k.a. metavariables).

foo(o) => {

Introduce type variable #o.

  a = o.fred |> toStr

Introduce #a, #fred, #res, add constraints
#o >= {fred: #fred}
((integer | string x) -> string) <= ((#fred) -> #res)
#a >= #res

Type checking & inference: how it works

  b = o.toto

Introduce type vars #b, #toto, add constraints
#o >= {toto: #toto}
#b >= #toto

  a = a.length

Introduce type vars #a2, #length, add constraints
#a >= {length: #length}
#a2 >= #length

Type checking & inference: how it works

  in if b then a else o.fred + 2

introduce type var #ari for o.fred + 2 and #t for the result, add constraints
#b <= boolean
#fred <= integer | number
integer <= integer | number
#ari >= #fred | integer
#t >= #a2 | #ari

Type checking & inference: how it works

  1. So now we have, grouping by the type var,
#o >= {fred: #fred}
#o >= {toto: #toto}
((integer | string x) -> string) <= ((#fred) -> #res)
#a >= #res
#a >= {length: #length}
#b >= #toto
#b <= boolean
#a2 >= #length
#fred <= integer | number
integer <= integer | number
#ari >= #fred | integer
#t >= #a2 | #ari

integer <= integer | number is obviously true, remove it

Type checking & inference: how it works

((integer | string x) -> string) <= ((#fred) -> #res)
is digested into smaller parts
string <= #res
#fred <= integer | string.

Combined with #fred <= integer | number
this gives #fred <= integer. We know #fred!

Combined with #res <= #a this gives #a >= string.
Which helps with #length - it should be integer.

#o >= {fred: #fred}
#o >= {toto: #toto}

combine into #o >= {fred: #fred, toto: #toto}.

Type checking & inference: how it works

#toto <= #b
#b <= boolean

gives #toto <= boolean. We know #toto!
So our function is (#o) -> #t where
#o >= {fred: #fred, toto: #toto}
and #fred <= integer
and #t >= #a2 | #ari where #ari >= #fred | integer and #a2 >= #length which is int.
So #t simplifies to integer and we have our answer:

foo: ({fred: integer, toto: boolean}) -> integer

Type checking & inference: how it works

> :st toStr
(integer | string x) -> string

foo(o) => {
  a = o.fred |> toStr
  b = o.toto
  a = a.length
  in if b then a else o.fred + 2
}

foo: ({fred: integer, toto: boolean}) -> integer.