1 of 26

Type Systems

Ken Q Pu, Faculty of Science, Ontario Tech University

2 of 26

Why types?

  1. Static analysis of code to prevent type related runtime errors.
  2. Static annotation of source code to improve code readability.

Let's first understand what a type system is.

Ken Q Pu, Faculty of Science, Ontario Tech University

3 of 26

Types

Types are descriptions of values.

Values can be:

  • Atomic scalars (numbers, strings, ...)
  • Composite data (records, tuples)
  • Containers (list, hashmap, arrays...)
  • Functions
  • Objects

Each value can be described by one or more types.

3

"Hello"

{:name "Einstein"

:IQ 160}

(defn add [x y]

(+ x y))

Integer

String

Record

:name String

:IQ Int

Function

(Num, Num) -> Num

Ken Q Pu, Faculty of Science, Ontario Tech University

4 of 26

Type Signature

"Hello"

{:name "Einstein"

:IQ 160}

(defn add [x y]

(+ x y))

String

Record

:name String

:IQ Int

Function

(Num, Num) -> Num

Expressions to be evaluated during runtime.

Type signature, or simply type of the expression, to be determined at compile time.

Ken Q Pu, Faculty of Science, Ontario Tech University

5 of 26

Type System

A type system is a formal sublanguage that can express the type signatures for all possible values supported by the programming language.

Ken Q Pu, Faculty of Science, Ontario Tech University

6 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

(+ pi

(inc 4)))

Ken Q Pu, Faculty of Science, Ontario Tech University

7 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

(+ pi

(inc 4)))

Float

Ken Q Pu, Faculty of Science, Ontario Tech University

8 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

(+ pi

(inc 4)))

Float

Float

Float

Ken Q Pu, Faculty of Science, Ontario Tech University

9 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

(+ pi

(inc 4 )))

Float

Float

Float

Int

Ken Q Pu, Faculty of Science, Ontario Tech University

10 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

(+ pi

(inc 4 )))

Float

Float

Float

Int

Int -> Int

Ken Q Pu, Faculty of Science, Ontario Tech University

11 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

(+ pi

(inc 4) ))

Float

Float

Float

Int

Ken Q Pu, Faculty of Science, Ontario Tech University

12 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

( + pi

(inc 4) ))

Float

Float

Float

Int

(Num, Num) -> Num

Ken Q Pu, Faculty of Science, Ontario Tech University

13 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

( + pi

(inc 4) ))

Float

Float

Float

Int

(Num, Num) -> Num

Num

Num

Ken Q Pu, Faculty of Science, Ontario Tech University

14 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

(+ pi

(inc 4)) )

Float

Float

Float

Ken Q Pu, Faculty of Science, Ontario Tech University

15 of 26

Statically typed language

A programming language is statically typed if all expressions in the source code have a valid type signature. Furthermore, the expression types must be determined before the program executes.

(let [pi 3.14]

(+ pi

(inc 4)))

Float

Computing the type signature of all expressions is called type inference.

​

Type inference is only done for statically typed languages. Dynamic typed languages computes the type signatures based on data values at runtime.

Ken Q Pu, Faculty of Science, Ontario Tech University

16 of 26

Clojure is not statically type.

Clojure compiler does not determine the type information of expressions during compile time.

All type information are determined at runtime.

(let [x (get-value ...)]

x)

Clojure only knows the type of x after get-value is executed.

Ken Q Pu, Faculty of Science, Ontario Tech University

17 of 26

Why types?

  • Static analysis of code to prevent type related runtime errors.
  • Static annotation of source code to improve code readability.

Ken Q Pu, Faculty of Science, Ontario Tech University

18 of 26

Runtime errors

Certain computation cannot be carried out at runtime, and the operating system has no choice but to stop the program execution immediately.

(let [x [:a :b :c]]

(println (nth x 5)))

(+ 3 "four")

Illegal data access. (nth x 5) cannot be evaluated because x only has three elements.

Illegal function invocation. Parameters of + cannot be mixed between numbers and strings.

Ken Q Pu, Faculty of Science, Ontario Tech University

19 of 26

Runtime errors are dangerous

Runtime errors can cause the system to be stuck in undesirable states.

The program can terminate prematurely beyond the expectation of the programmer.

(defn move-file [source target]

(let [content (read-file source)]

(remove-file source)

(println (+ "Bytes to move: " (count content)))

(write-file target content)))

What is the runtime behaviour?

​

(move-file "important.txt"

"passwords.txt")

Ken Q Pu, Faculty of Science, Ontario Tech University

20 of 26

Static Analysis: type checking

Type checking is the verification that all expressions have valid types.

More details will be discussed on the type checking algorithm.

( + "Bytes to move: " ( count content ) )

Ken Q Pu, Faculty of Science, Ontario Tech University

21 of 26

Static Analysis: type checking

( + "Bytes to move: " ( count content ) )

Array ✔

Iterable ✔

Ken Q Pu, Faculty of Science, Ontario Tech University

22 of 26

Static Analysis: type checking

( + "Bytes to move: " ( count content ) )

Iterable -> Int ✔

Ken Q Pu, Faculty of Science, Ontario Tech University

23 of 26

Static Analysis: type checking

( + "Bytes to move: " ( count content ) )

Iterable -> Int ✔

Iterable ✔

Ken Q Pu, Faculty of Science, Ontario Tech University

24 of 26

Static Analysis: type checking

( + "Bytes to move: " ( count content ) )

Iterable -> Int ✔

Iterable ✔

Int ✔

Ken Q Pu, Faculty of Science, Ontario Tech University

25 of 26

Static Analysis: type checking

( + "Bytes to move: " ( count content ) )

Int ✔

String ✔

Int, Int -> Int

or

String, String -> String

Ken Q Pu, Faculty of Science, Ontario Tech University

26 of 26

Static Analysis: type checking

( + "Bytes to move: " ( count content ) )

Int ✔

String ✔

Int, Int -> Int

or

String, String -> String

ERROR ✖

Ken Q Pu, Faculty of Science, Ontario Tech University