Types I: type systems and type checking

# A type checker for the simply typed lambda calculus with integers, Booleans,
# conditionals, let and pairs.  Types: "int" | "bool" | ("->", t1, t2) | ("*", t1, t2)
#   e ::= n | True | False | x | ("+", e, e) | ("<", e, e) | ("if", e, e, e)
#       | ("lam", x, t, e) | ("app", e, e) | ("let", x, e, e) | ("pair", e, e) | ("fst", e) | ("snd", e)
def show(t):
    if isinstance(t, str): return t
    if t[0] == "->": return f"({show(t[1])} -> {show(t[2])})"
    return f"({show(t[1])} * {show(t[2])})"

class TypeError_(Exception): pass

def check(env, e, depth=0, trace=None):
    def note(t):
        if trace is not None: trace.append("  " * depth + f"⊢ {brief(e)} : {show(t)}")
        return t
    if isinstance(e, bool): return note("bool")
    if isinstance(e, int):  return note("int")
    if isinstance(e, str):
        if e not in env: raise TypeError_(f"unbound variable {e}")
        return note(env[e])
    tag = e[0]
    sub = lambda env2, x: check(env2, x, depth + 1, trace)
    if tag in ("+", "<"):
        for side in (e[1], e[2]):
            if sub(env, side) != "int": raise TypeError_(f"operand of {tag} must be int")
        return note("int" if tag == "+" else "bool")
    if tag == "if":
        if sub(env, e[1]) != "bool": raise TypeError_("condition must be bool")
        t1, t2 = sub(env, e[2]), sub(env, e[3])
        if t1 != t2: raise TypeError_(f"branches differ: {show(t1)} vs {show(t2)}")
        return note(t1)
    if tag == "lam":
        _, x, tx, body = e
        return note(("->", tx, sub({**env, x: tx}, body)))
    if tag == "app":
        tf, ta = sub(env, e[1]), sub(env, e[2])
        if not (isinstance(tf, tuple) and tf[0] == "->"): raise TypeError_(f"applying a non-function of type {show(tf)}")
        if tf[1] != ta: raise TypeError_(f"argument has type {show(ta)}, expected {show(tf[1])}")
        return note(tf[2])
    if tag == "let":
        return note(sub({**env, e[1]: sub(env, e[2])}, e[3]))
    if tag == "pair": return note(("*", sub(env, e[1]), sub(env, e[2])))
    if tag in ("fst", "snd"):
        t = sub(env, e[1])
        if not (isinstance(t, tuple) and t[0] == "*"): raise TypeError_("fst/snd of a non-pair")
        return note(t[1] if tag == "fst" else t[2])

def brief(e):
    s = str(e).replace("'", "")
    return s if len(s) <= 34 else s[:31] + "..."

twice = ("lam", "f", ("->", "int", "int"), ("lam", "x", "int", ("app", "f", ("app", "f", "x"))))
inc = ("lam", "n", "int", ("+", "n", 1))
prog = ("app", ("app", twice, inc), 5)
tr = []
print("type:", show(check({}, prog, trace=tr)))
print("derivation (premises indented under conclusions, conclusions printed last):")
print("\n".join(tr[-6:]))
for bad in [("if", 1, 2, 3), ("app", inc, True), ("+", 1, ("lam", "x", "int", "x")), ("app", 5, 5)]:
    try:
        check({}, bad)
    except TypeError_ as err:
        print(f"rejected {brief(bad):30} -> {err}")

type: int
derivation (premises indented under conclusions, conclusions printed last):
        ⊢ 1 : int
      ⊢ (+, n, 1) : int
    ⊢ (lam, n, int, (+, n, 1)) : (int -> int)
  ⊢ (app, (lam, f, (->, int, int), ... : (int -> int)
  ⊢ 5 : int
⊢ (app, (app, (lam, f, (->, int, ... : int
rejected (if, 1, 2, 3)                  -> condition must be bool
rejected (app, (lam, n, int, (+, n, 1)),... -> argument has type bool, expected int
rejected (+, 1, (lam, x, int, x))       -> operand of + must be int
rejected (app, 5, 5)                    -> applying a non-function of type int

# Type soundness, tested: generate random well-typed closed terms, evaluate them with a
# small-step evaluator, and confirm none gets stuck and every result has the predicted type.
import random
rnd = random.Random(11)

def gen(t, env, d):
    """A random term of type t ("int" or "bool") using variables in env."""
    choices = [v for v, tv in env.items() if tv == t]
    if d == 0 or rnd.random() < 0.25:
        if choices and rnd.random() < 0.5: return rnd.choice(choices)
        return rnd.randint(0, 9) if t == "int" else rnd.choice([True, False])
    k = rnd.random()
    if t == "int" and k < 0.4: return ("+", gen("int", env, d - 1), gen("int", env, d - 1))
    if t == "bool" and k < 0.4: return ("<", gen("int", env, d - 1), gen("int", env, d - 1))
    if k < 0.7: return ("if", gen("bool", env, d - 1), gen(t, env, d - 1), gen(t, env, d - 1))
    x = f"v{d}{rnd.randint(0, 99)}"; tx = rnd.choice(["int", "bool"])
    return ("app", ("lam", x, tx, gen(t, {**env, x: tx}, d - 1)), gen(tx, env, d - 1))

def is_value(e): return isinstance(e, (int, bool)) and not isinstance(e, str) or (isinstance(e, tuple) and e[0] == "lam")
def subst(e, x, v):
    if isinstance(e, str): return v if e == x else e
    if not isinstance(e, tuple): return e
    if e[0] == "lam": return e if e[1] == x else ("lam", e[1], e[2], subst(e[3], x, v))
    return (e[0],) + tuple(subst(a, x, v) for a in e[1:])
def step(e):
    tag = e[0]
    if tag in ("+", "<"):
        if not is_value(e[1]): return (tag, step(e[1]), e[2])
        if not is_value(e[2]): return (tag, e[1], step(e[2]))
        return e[1] + e[2] if tag == "+" else e[1] < e[2]
    if tag == "if":
        if not is_value(e[1]): return ("if", step(e[1]), e[2], e[3])
        return e[2] if e[1] is True else e[3]
    if tag == "app":
        if not is_value(e[1]): return ("app", step(e[1]), e[2])
        if not is_value(e[2]): return ("app", e[1], step(e[2]))
        return subst(e[1][3], e[1][1], e[2])
    raise RuntimeError(f"stuck: {e}")      # progress says this never happens for well-typed terms

stuck = wrong_type = steps = 0
for i in range(3000):
    t = rnd.choice(["int", "bool"]); e = gen(t, {}, 5)
    try:
        while not is_value(e):
            e = step(e); steps += 1
        if (t == "bool") != isinstance(e, bool): wrong_type += 1
    except RuntimeError:
        stuck += 1
print(f"3000 random well-typed terms, {steps} steps in total")
print(f"stuck terms: {stuck}   results of the wrong type: {wrong_type}")

3000 random well-typed terms, 29430 steps in total
stuck terms: 0   results of the wrong type: 0

enum Shape { Circle(f64), Square(f64), Triangle(f64, f64) }

fn area(s: &Shape) -> f64 {
    // the Triangle case has been forgotten
    match s { Shape::Circle(r) => 3.14159 * r * r, Shape::Square(a) => a * a }
}

fn main() {
    println!("{}", area(&Shape::Square(2.0)));
}

error[E0004]: non-exhaustive patterns: `&Shape::Triangle(_, _)` not covered
 --> main.rs:5:11
  |
5 |     match s { Shape::Circle(r) => 3.14159 * r * r, Shape::Square(a) => a * a }
  |           ^ pattern `&Shape::Triangle(_, _)` not covered
  |
note: `Shape` defined here
 --> main.rs:1:6
  |
1 | enum Shape { Circle(f64), Square(f64), Triangle(f64, f64) }
  |      ^^^^^                             -------- not covered
  = note: the matched value is of type `&Shape`
help: ensure that all possible cases are being handled by adding a match arm with a wildcard pattern or an explicit pattern as shown
  |
5 |     match s { Shape::Circle(r) => 3.14159 * r * r, Shape::Square(a) => a * a, &Shape::Triangle(_, _) => todo!() }
  |                                                                             +++++++++++++++++++++++++++++++++++
error: aborting due to 1 previous error
For more information about this error, try `rustc --explain E0004`.

from typing import Optional

def find_user(uid: int) -> Optional[str]:
    return {1: "ada", 2: "grace"}.get(uid)

def greeting(uid: int) -> str:
    name = find_user(uid)
    return "Hello, " + name.title()      # name might be None

def greeting_fixed(uid: int) -> str:
    name = find_user(uid)
    if name is None:
        return "Hello, stranger"
    return "Hello, " + name.title()      # narrowed to str here

$ mypy --strict users.py
users.py:8: error: Item "None" of "str | None" has no attribute "title"  [union-attr]

public class Covariance {
    public static void main(String[] args) {
        String[] names = {"Ada", "Grace"};
        Object[] things = names;          // allowed: arrays are covariant in Java
        try {
            things[0] = Integer.valueOf(42);   // type checks statically...
        } catch (ArrayStoreException e) {
            System.out.println("run-time check caught it: " + e);
        }
        System.out.println("names[0] is still " + names[0]);
    }
}

run-time check caught it: java.lang.ArrayStoreException: java.lang.Integer
names[0] is still Ada

function total(xs: number[]): number {
  return xs.reduce((a, b) => a + b, 0);
}
const fromNetwork: any = JSON.parse('["1", "2", "3"]');   // really strings
console.log(total(fromNetwork));                            // compiles; prints a string

$ tsc --strict --target es2020 total.ts
$ node total.js
0123