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.]
1
Type Checking Basics
CSI 3120
Amy Felty University of Ottawa
slides copyright 2017, 2018, 2019, 2020 Author David Walker, updated by Amy Felty permission granted to reuse these slides for non-commercial educational purposes
2
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:
4
2 : int “hello” : string
2 + 2 : int “I say ” ^ “hello” : string
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!)
– atfirstyoumayfindthistobeapain…
• 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
• Example rules:
(1)
(2) “abc” : string
0 : int
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
6
• Example rules:
(1)
(2) “abc” : string
0 : int
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
7
(3) ife1:intande2:int (4) ife1:intande2:int
then e1 + e2 : int then e1 * e2 : int
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string then e1 ^ e2 : string
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
8
if e : int
then string_of_int e : string
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string
• Using the rules: 2:intand3:int.
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
9
(Byrule 1)
if e : int
then string_of_int e : string
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string • Using the rules:
2:intand3:int. Therefore, (2 + 3) : int
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
10
(Byrule 1) (By rule 3)
if e : int
then string_of_int e : string
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string • Using the rules:
2:intand3:int. Therefore, (2 + 3) : int 5 : int
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
11
(Byrule 1) (By rule 3) (By rule 1)
if e : int
then string_of_int e : string
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
FYI: This is a formal proof (4) ife1:intande2:int
then e1 + e2 : int
if e1 : string and e2 : string
(6)
(5)
• Using the rules:
then e1 ^ e2 : string
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
12
(Byrule 1) (By rule 3) (By rule 1)
that the expression is well-
then e1 * e2 : int typed!
if e : int
then string_of_int e : string
2:intand3:int.
Therefore, (2 + 3) : int
5 : int
Therefore, (2 + 3) * 5 : int (By rule 4 and our previous work)
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string
• Another perspective:
rule (4) for typing expressions says I can put any expression with type int in place of the ????
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
13
if e : int
then string_of_int e : string
???? * ???? : int
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string
• Another perspective:
rule (4) for typing expressions says I can put any expression with type int in place of the ????
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
14
7
if e : int
then string_of_int e : string
* ???? :int
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string
• Another perspective:
rule (4) for typing expressions says I can put any expression with type int in place of the ????
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
15
7
if e : int
then string_of_int e : string
* (add_one 17) : int
Type Checking Rules
• You can always start up the OCaml interpreter to find out a type of a simple expression:
16
$ ocaml
OCaml Version 4.07.0
#
Type Checking Rules
• You can always start up the OCaml interpreter to find out a type of a simple expression:
17
$ ocaml
OCaml Version 4.07.0
# 3 + 1;;
Type Checking Rules
• You can always start up the OCaml interpreter to find out a type of a simple expression:
press return and you find out the type and the value
18
$ ocaml
OCaml Version 4.07.0
# 3 + 1;;
– : int = 4 #
Type Checking Rules
• You can always start up the OCaml interpreter to find out a type of a simple expression:
press return and you find out the type and the value
19
$ ocaml
OCaml Version 4.07.0
# 3 + 1;;
– : int = 4
# “hello ” ^ “world”;;
– : string = “hello world” #
Type Checking Rules
• You can always start up the OCaml interpreter to find out a type of a simple expression:
20
$ ocaml
OCaml Version 4.07.0
# 3 + 1;;
– : int = 4
# “hello ” ^ “world”;;
– : string = “hello world” # #quit;;
$
• Example rules:
(1)
(2) “abc” : string
0 : int
(3) ife1:intande2:int
then e1 + e2 : int
(5) if e1 : string and e2 : string
then e1 ^ e2 : string • Violating the rules:
“hello” : string 1 : int
1 + “hello” : ??
(4) ife1:intande2:int then e1 * e2 : int
(6)
Type Checking Rules
(and similarly for any other integer constant n) (and similarly for any other string constant “…”)
21
if e : int
then string_of_int e : string
(By rule 2)
(By rule 1)
(NO TYPE! Rule 3 does not apply!)
•
•
Violating the rules:
Type Checking Rules Violating the rules:
22
# “hello” + 1;;
Error: This expression has type string but an
expression was expected of type int
• • •
• • •
The type error message tells you the type that was expected The type error message tells you the type that was expected
and the type that it inferred for your subexpression and the type that it inferred for your subexpression
By the way, this was one of the nonsensical expressions that
By the way, this was one of the nonsensical expressions that
did not evaluate to a value
did not evaluate to a value
It is a good thing that this expression does not type check! 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:
23
# “hello” + 1;;
Error: This expression has type string but an
expression was expected of type int
• A possible fix:
# “hello” ^ (string_of_int 1);;
– : string = “hello1”
• One of the keys to becoming a good ML programmer is to understand type error messages.
Example Type-checking Rules
24
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)
Type Checking Rules
• Type errors for if statements can be confusing sometimes. Example: We create a string from s, concatenating it n times:
25
let rec concatn s n = if n <= 0 then
... else
s ^ (concatn s (n-1))
Type Checking Rules
• Type errors for if statements can be confusing sometimes. Example. We create a string from s, concatenating it n times:
OCaml says:
26
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
Type Checking Rules
• Type errors for if statements can be confusing sometimes. Example. We create a string from s, concatenating it n times:
OCaml says:
27
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
•
Type Checking Rules
Type errors for if statements can be confusing sometimes. Example. We create a string from s, concatenating it n times:
they don't agree!
OCaml says:
28
let rec concatn s n = 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
•
29
Type Checking Rules
Type errors for if statements can be confusing sometimes. Example. We create a string from s, concatenating it n times:
they don't agree!
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.
let rec concatn s n = if n <= 0 then
0
else
s ^ (concatn s (n-1))
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:
32
# 3 / 0 ;;
Exception: Division_by_zero.
• Why doesn't the ML type checker do us the favor of telling us the expression will raise an exception?
Type Checking Rules • What about this expression:
33
# 3 / 0 ;;
Exception: Division_by_zero.
• 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:
# 3 / (if turing_machine_halts m then 0 else 1);;
• There are type systems that will rule out divide-by-zero errors, but they require programmers to supply proofs to the type checker
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
Robin Milner
• The type error message tells you the type that was expected
3. CCS, a general theory of concurrency.
and the type that it inferred for your subexpression
In addition, he formulated and strongly advanced full abstraction, the study of
• By the way, this was one of the nonsensical expressions that the relationship between operational and denotational semantics.”
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
36
Well typed programs do not go wrong
• Violating the rules:
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;
SUMMARY
37
38
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