CSI3120 A
1
For a short humorous talk on
languages without strong typing:
https://www.destroyallsoftware.com/talks/wat
[Broader point: No one (few people) knows what
their programs do in untyped languages.]
http://www.destroyallsoftware.com/talks/wat
Type Checking Basics
2
slides copyright 2017, 2018, 2019, 2020
Author David Walker, updated by Amy Felty
permission granted to reuse these slides for non-commercial educational purposes
Last Time
Functional programming history
– Church & the lambda calculus
– Scheme
– ML (OCaml)
– Modern times: F#, Clojure, Scala, Map-Reduce, …
OCaml
– Functional language, gets most work done by analyzing old data and
producing new, immutable data
– Simple, typed programming language based on the lambda calculus
– Immutable data is the default; mutable data is possible (imperative,
object-oriented)
3
Type Checking
• Every value has a type and so does every expression
• This is a concept that is familiar from Java but it becomes
more important when programming in a functional language
• The type of an expression is determined by the type of its
subexpressions
• We write (e : t) to say that expression e has type t. eg:
2 : int “hello” : string
2 + 2 : int “I say ” ^ “hello” : string
4
Type Checking Rules
• There are a set of simple rules that govern type checking
– programs that do not follow the rules will not type check and
OCaml will refuse to compile them for you (the nerve!)
– at first you may find this to be a pain …
• But types are a great thing:
– they help us think about how to construct our programs
– they help us find stupid programming errors
– they help us track down compatibility errors quickly when we
edit and maintain our code
– they allow us to enforce powerful invariants about our data
structures
5
Type Checking Rules
• Example rules:
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
6
Type Checking Rules
• Example rules:
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
7
Type Checking Rules
• Example rules:
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
8
Type Checking Rules
• Example rules:
• Using the rules:
2 : int and 3 : int.
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
(By rule 1)
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
9
Type Checking Rules
• Example rules:
• Using the rules:
2 : int and 3 : int.
Therefore, (2 + 3) : int
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
(By rule 1)
(By rule 3)
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
10
Type Checking Rules
• Example rules:
• Using the rules:
2 : int and 3 : int.
Therefore, (2 + 3) : int
5 : int
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
(By rule 1)
(By rule 3)
(By rule 1)
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
11
Type Checking Rules
• Example rules:
• Using the rules:
2 : int and 3 : int.
Therefore, (2 + 3) : int
5 : int
(3) if e1 : int and e2 : int
then e1 + e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
(By rule 1)
(By rule 3)
(By rule 1)
Therefore, (2 + 3) * 5 : int (By rule 4 and our previous work)
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
(
F
4
Y
)
I:
if
T
e
h
1
is
:i
i
n
s
t
a
an
fo
d
r
e
m
2
a
:i
l
n
p
t
roof
that tthheeneex1p*ree2ss: iiontn is well-
typed!
12
Type Checking Rules
• Example rules:
• Another perspective:
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
???? * ???? : int
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
rule (4) for typing expressions
says I can put any expression
with type int in place of the ????
13
Type Checking Rules
• Example rules:
• Another perspective:
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
7 * ???? : int
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
rule (4) for typing expressions
says I can put any expression
with type int in place of the ????
14
Type Checking Rules
• Example rules:
• Another perspective:
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
7 * (add_one 17) : int
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
rule (4) for typing expressions
says I can put any expression
with type int in place of the ????
15
Type Checking Rules
• You can always start up the OCaml interpreter to find out a
type of a simple expression:
$ ocaml
OCaml Version 4.07.0
#
16
Type Checking Rules
• You can always start up the OCaml interpreter to find out a
type of a simple expression:
$ ocaml
OCaml Version 4.07.0
# 3 + 1;;
17
Type Checking Rules
• You can always start up the OCaml interpreter to find out a
type of a simple expression:
$ ocaml
OCaml Version 4.07.0
# 3 + 1;;
– : int = 4
#
press
return
and you
find out
the type
and the
value
18
Type Checking Rules
• You can always start up the OCaml interpreter to find out a
type of a simple expression:
$ ocaml
OCaml Version 4.07.0
# 3 + 1;;
– : int = 4
# “hello ” ^ “world”;;
-: string = “hello world”
#
press
return
and you
find out
the type
and the
value
19
Type Checking Rules
• You can always start up the OCaml interpreter to find out a
type of a simple expression:
$ ocaml
OCaml Version 4.07.0
# 3 + 1;;
– : int = 4
# “hello ” ^ “world”;;
-: string = “hello world”
# #quit;;
$
20
Type Checking Rules
• Example rules:
• Violating the rules:
“hello” : string
1 : int
1 + “hello” : ??
(3) if e1 : int and e2 : int (4)
then e1 + e2 : int
if e1 : int and e2 : int
then e1 * e2 : int
if e1 : string and e2 : string
then e1 ^ e2 : string
if e : int
then string_of_int e : string
(By rule 2)
(By rule 1)
(NO TYPE! Rule 3 does not apply!)
0 : int (and similarly for any other integer constant n)
(2) “abc” : string (and similarly for any other string constant “…”)
(1)
(5) (6)
21
• The type error message tells you the type that was expected
and the type that it inferred for your subexpression
• By the way, this was one of the nonsensical expressions that
did not evaluate to a value
• It is a good thing that this expression does not type check!
“Well typed programs do not go wrong”
Robin Milner, 1978
Type Checking Rules
• Violating the rules:
# “hello” + 1;;
Error: This expression has type string but an
expression was expected of type int
22
Type Checking Rules
• Violating the rules:
• A possible fix:
• One of the keys to becoming a good ML programmer is to
understand type error messages.
# “hello” + 1;;
Error: This expression has type string but an
expression was expected of type int
# “hello” ^ (string_of_int 1);;
– : string = “hello1”
23
Example Type-checking Rules
if e1 : bool
and e2 : t and e3 : t (the same type t, for some type t)
then if e1 then e2 else e3 : t (that same type t)
24
Type Checking Rules
• Type errors for if statements can be confusing sometimes.
Example: We create a string from s, concatenating it n times:
let rec concatn s n =
if n <= 0 then ... else s ^ (concatn s (n-1)) 25 Type Checking Rules • Type errors for if statements can be confusing sometimes. Example. We create a string from s, concatenating it n times: let rec concatn s n = if n <= 0 then ... else s ^ (concatn s (n-1)) Error: This expression has type int but an expression was expected of type string OCaml says: 26 • Type errors for if statements can be confusing sometimes. Example. We create a string from s, concatenating it n times: Type Checking Rules Error: This expression has type int but an expression was expected of type string let rec concatn s n = if n <= 0 then ... else s ^ (concatn s (n-1)) OCaml says: 27 • Type errors for if statements can be confusing sometimes. Example. We create a string from s, concatenating it n times: Type Checking Rules Error: This expression has type int but an expression was expected of type string let rec concatn s n = if n <= 0 then 0 else s ^ (concatn s (n-1)) OCaml says: they don't agree! 28 • Type errors for if statements can be confusing sometimes. Example. We create a string from s, concatenating it n times: Type Checking Rules let rec concatn s n = if n <= 0 then 0 else s ^ (concatn s (n-1)) The type checker points to the correct branch as the cause of an error because it does not AGREE with the type of an earlier branch. Really, the error is in the earlier branch. Moral: Sometimes you need to look in an earlier branch for the error even though the type checker points to a later branch. The type checker doesn't know what the user wants. they don't agree! 29 A Tactic: Add Typing Annotations 30 let rec concatn (s:string) (n:int) : string = if n <= 0 then 0 else s ^ (concatn s (n-1)) Error: This expression has type int but an expression was expected of type string EXCEPTIONS: DO THEY CAUSE PROGRAMS TO "GO WRONG"? 31 Type Checking Rules • What about this expression: • Why doesn't the ML type checker do us the favor of telling us the expression will raise an exception? # 3 / 0 ;; Exception: Division_by_zero. 32 Type Checking Rules • What about this expression: • Why doesn't the ML type checker do us the favor of telling us the expression will raise an exception? – In general, detecting a divide-by-zero error requires we know that the divisor evaluates to 0. – In general, deciding whether the divisor evaluates to 0 requires solving the halting problem: • There are type systems that will rule out divide-by-zero errors, but they require programmers to supply proofs to the type checker # 3 / 0 ;; Exception: Division_by_zero. # 3 / (if turing_machine_halts m then 0 else 1);; 33 Isn’t that cheating? “Well typed programs do not go wrong” Robin Milner, 1978 (3 / 0) is well typed. Does it “go wrong?” Answer: No. “Go wrong” is a technical term meaning, “have no defined semantics.” Raising an exception is perfectly well defined semantics, which we can reason about, which we can handle in ML with an exception handler. So, it’s not cheating. 34 Type Soundness “Well typed programs do not go wrong” Programming languages with this property have sound type systems. They are called safe languages. Safe languages are generally immune to buffer overrun vulnerabilities, uninitialized pointer vulnerabilities, etc. (but not immune to all bugs!) Safe languages: ML, Java, Python, … Unsafe languages: C, C++, Pascal 35 Well typed programs do not go wrong “Well typed programs do not go wrong” Robin Milner, 1978 Robin Milner Turing Award, 1991 “For three distinct and complete achievements: 1.LCF, the mechanization of Scott's Logic of Computable Functions, probably the first theoretically based yet practical tool for machine assisted proof construction; 2.ML, the first language to include polymorphic type inference together with a type-safe exception-handling mechanism; 3. CCS, a general theory of concurrency. In addition, he formulated and strongly advanced full abstraction, the study of the relationship between operational and denotational semantics.” 36 SUMMARY 37 OCaml OCaml is a functional programming language – Java gets most work done by modifying data – OCaml gets most work done by producing new, immutable data OCaml is a typed programming language – the type of an expression correctly predicts the kind of value the expression will generate when it is executed – there are systematic rules defining when any expression (or program) type checks • these rules actually form a formal logic ... it is not a coincidence that languages like ML are used inside theorem provers – the type system is sound; the language is safe 38