Open with https://github.com/maaslalani/slides/

schasm-type-inference-slides.md

Static type checking for the Algorithmic Language Scheme

Authors:

• Nikita Medvedev
• Anton Zavyalov

---

Prerequirements

• Schasm - Scheme to WebAssembly compiler
  • Software Development Tech course, 2021
• Scheme - dynamically typed minimal Lisp dialect

Goals

• Type checking
• Type inference
• Expressiveness comparable with original Scheme type system
• New knowledge about compilers and type theory

---

Gradual typing

Full-fledged static typing

Pros:

• Soundness (rejects all incorrect programs)

Cons:

• Incompleteness (there are correct programs, which are also rejected)

Solution - gradual typing:

;; Dynamically typed code
(display (+ 21 "Twenty one"))

;; Typed code block
(begin-typed
    (display (+ 21 "Twenty one"))) ;; Error: cannot unify Number with String

---

Type checking and type inference

Type checking

Pretty simple to implement with explicit type annotations:

(: foo Number)
(: bar String)
(: check-number (-> Number Nil))

(check-number foo)
(check-number bar) ;; Error: cannot unify Number with String

Type inference

Infer exact types from expressions and check with implicit type annotations:

(define foo 21)                       ;; Number
(define bar "Twenty one")             ;; String
(define (check-number x) (+ x 0) '()) ;; Number -> Nil

(check-number foo)
(check-number bar) ;; Error: cannot unify Number with String

Hindley-Milner type system and inference algorithm

---

Hindley-Milner type system (for Scheme)

Types

• A = Elementary type | (A*) -> A | (Cons A A)
• Elementary type = Nil | Number | String | Symbol

Inference rules (with immediate resolution)

• Var: e |- x ~> A, Ø if e contains x: A;
• Const: e |- t ~> Elementary type, Ø;
• App: e |- t u ~> σ X, σ ○ ρ' ○ ρ if e |- u ~> A, ρ, e |- t ~> B, ρ', σ = mgu(B = ρ'A -> X);
• Lam: e |- fun x -> t ~> (ρX -> A), ρ, if (e, x:X) |- t ~> A, ρ;
• Cons: just as Lam, but with (Cons _ _) instead of _ -> _;
• If: e |- if t then u else v ~> σC, σ ○ ρ'' ○ ρ' ○ ρ, if e |- ~> A, ρ, ρe |- u ~> B, ρ', ρ'ρe |- v ~> C, ρ'', σ = mgu(ρ''B = C);
• Let: e |- let x = t in u ~> B, ρ' ○ ρ if e |- t ~> A, ρ, (ρe, x:A) |- u ~> B, ρ'.

Unification

mgu(X = Y) here stands for "Most general unifier". It can be setted inductively with Robinson algorithm:

• ∅, if X == Y, X - elementary type;
• {X/Y}, if X - type variable, Y/X, if Y - type varaible;
• {X2/Y2} ○ {X1/Y1}, if X = X1 -> X2, Y = Y1 -> Y2, OR, if X and Y are Cons with same compound type variables;
• otherwise, cannot unify X and Y.

---

Features and restrictions

Let-polymorphism

(define (i x) x)      ;; a -> a
(i 21)                ;; Number
(i "Twenty one")      ;; String
(i (cons 'hello '())) ;; (Cons Symbol Nil)

Explicit declarations of recursive functions

(: factorial (-> Number Number))         ;; (1)
(define (factorial n)
  (if (<= n 1) 1 (* factorial (- n 1)))) ;; Will raise error if (1) isn't presented

• Can solve with special Fix inference rule
• Fix rule still cannot handle mutual recursion
• With efficient implementation of Fix rule type checker becames multi-pass

No way to handle lists and heterogeneous data (just as in plain Scheme)

(if #t '(1 2 3) '())   ;; Error: cannot unify (Cons Number (Cons Number Nil)) with Nil

(if #t "Hello" 'world) ;; Error: cannot unify String with Symbol

Problem of mutation of polymorphic references

OCaml:

let x = ref (fun x -> x) in
(x := fun x -> 10); !x "Hello" (* Error: This expression has type string but an expression was expected of type int *)

Schasm:

(define x (lambda (x) x)) ;; x : a -> a
(set! x (lambda (x) 10))
(x "Hello")               ;; ???

---

Lists and union types

Lists

• List a = Nil | Cons a (List a)
• If-List inference rule
• Type variable unification

Example:

(if #t
  '(1 2 3)
  '()) ;; List Number

(if #t
  '(a b c d)
  (cons 'a '())) ;; List Symbol

(if #t (cons "Foo" '()) '()) ;; List String

Unions

• Union t1 ... tn = t1 | ... | tn
• If-Union inference rule

Example:

(if #t "twenty one" 21)                     ;; (Union Number String)
(cond ((c1 'foo) (c2 "bar") (else '(baz)))) ;; (Union Symbol String (Cons Symbol Nil))

How to retreive exact value from list or union?

(define x (if #t '(1) '())) ;; List Number
(if ((pair? x)
    (check-number (car x))
    (check-nil x)))

(define y (if #t 1 'one)) ;; (Union Number Symbol)
(if ((number? x)
    (check-number x)
    (check-symbol x)))

---

Occurrence typing

• Kotlin:

val x: Any = if (Math.random() > 0.5) 1 else "one"
when (x) {
   is Int -> println(x + 10)
   is String -> println(x)
}

• TypeScript:

const x: 1 | "one" = (Math.random() > 0.5) ? 1 : "one";
if (typeof x == "number") {
    console.log(x + 10);
} else {
    console.log(x);
}

• Typed Racket

Proposition types

• Type predicates: number?, string?, symbol?, pair?, nil?
• If an argument of (predicate x) is a reference, returns not boolean, but Proposition x testing-type (unifiable with boolean)
• If-Proposition inference rule: If c in (if c t f) form is Proposition x a, then enrich scope of t with x -> a, f with x -> (not a)
• not a for union type a is a complement for it, for one of instances of List type is Cons and Nil respectively

---

Mutation of polymorphic references

(define x (lambda (x) x)) ;; x : a -> a
(set! x (lambda (x) 10))
(x "Hello")               ;; ???

Ways to resolve:

• Prohibit such assignments
• Rectify type of original reference every time set! occurs
• X. Leroy, P. Weis. Polymorphic type inference and assignment

Reference type rectification:

(: x a)
(: y a)

(if #t
  (set! x 10)    ;; x : Number
  (set! x 'foo)) ;; Error: cannot unify Number with Symbol

(define (mutator)
  (set! y "Mutated")) ;; y : String

(set! y 'bar)    ;; Error: cannot unify String with Symbol

---

Dealing with type hierarchies

• With lists and unions we introduced subtypes:
  • List a <: Nil, Cons a, List a
  • Union x y z <: x, y, z, Union x y, Union y z, Union x z, Union x y z
• Moreover: a <: Nil, String, Number, Symbol, ...
• But our unification algorithm for now treats elements in separate inheritance branches as equal (Cons a === Nil)
• Solution: unification according to type hierarchy
  • x unifies with y => x <: y

Example:

(: f (-> (List String) Nil))
(: x (Cons String Nil))
(f x)

(: g (-> (Cons String Nil) Nil))
(: y (List String))

(g y) ;; Error: cannot unify (Cons String Nil) with (List string)

(: h1 (-> a Nil))
(: z1 Number)
(h1 z1)

(: h2 (-> Number Nil))
(: z2 a)
(h2 z2) ;; Error: prohibited instantiation of a to Number

---

Conclusion

• Almost sound, allows to typecheck a quite big subset of Scheme programs - seems as good trade-off
• Hindley-Milner type system as kernel
• Lists, union types, occurrence typing
• Simple inference rule for mutable references

References

• D. S. Miginsky. Type inference
• Stephen Diehl, Write You a Haskell (http://dev.stephendiehl.com/fun/)
• Daniel Fedorin, Compiling a Functional Language Using C++, Part 10 - Polymorphism (https://danilafe.com/blog/10_compiler_polymorphism/)
• Gilles Dowek, Jean-Jacques L´evy. Introduction to the Theory of Programming Languages, Springer-Verlag London Limited, 2011
• Benjamin C. Pierce. Types and Programming Languages, MIT Press, 2002
• X. Leroy, P. Weis. Polymorphic type inference and assignment