4Types
CS 381 • Typing
1
CS 381 • Typing
2
4Types
Types,Type Errors,Type Systems Why Type Checking?
Static vs. Dynamic Typing Polymorphism
Parametric Polymorphism
Lost …
CS 381 • Typing
mars.jpl.nasa.gov/msp98/orbiter/
3
CS 381 • Typing
4
More Motivation …
Video clip
First-Cause Arguments
Kalam Cosmological Argument (Al-Ghazali,William Lane Craig, …)
(1)Whatever begins to exist has a cause. (2) The Universe began to exist.
(3) Therefore, the Universe had a cause.
Plato, Aristotle, Aquinas, …
CS 381 • Typing
5
Fallacy of Composition
Composition Fallacy
Incorrect Reasoning
Individual things a, b, c, … of type A have property P. Therefore, A has property P.
✗
Atoms are invisible
Therefore, cats are invisible. ✗
. Cats are made of atoms.
Every natural number has a successor. Therefore, the type Nat has a successor.
Confusing ✗ types & values
Everything in the universe has a cause.
CS 381 • Typing Therefore, the universe has a cause. 6
CS 381 • Typing
7
> “5” – 3 2
> “5” + 3 53
> 5 + “3” 53
> 5 + +”3″ 8
> “5” + +”3″ 53
> “5” + +”3″ – 2 51
> “5” + +”3″ + – 2 53-2
> “foo” + +”foo” fooNaN
> +”foo” + +”foo” NaN
> +”foo” + “foo” NaNfoo
JavaScript Madness
CS 381 • Typing
8
What is a Type (System)?
•Type
Collection of PL elements that share the same behavior
•Type System
Formal system to characterize the types of PL elements and their interactions
Can be used to prove the absence of type errors
•Purpose ofType Systems
Ensure meaningful interaction of different program parts, i.e., ensure absence of type errors
CS 381 • Typing
9
Type Errors
•Type Error
Illegal combination of PL elements
(typically: applying an operation to a value of the wrong type)
•Why are type errors bad?
Lead to program crashes Cause incorrect computations
CS 381 • Typing
10
Why Types are a Good Thing
(1) Types provide precise documentation of programs
(2) Types summarize a program on an abstract level
(3)Type correctness means partial correctness of programs; a type checker delivers partial correctness proofs
(4) Type systems can prevent runtime errors (and can save a lot of debugging)
(5) Type information can be exploited for optimization
Things to Know About Type Systems
(1) Notion of Type Safety
(2) Strong vs.Weak Typing
(3)Static vs.“DynamicTyping”
(4) Approximation & Undecidability of Static Typing (5) Type Checking vs.Type Inference
(6) Polymorphism (parametric, subtype, ad hoc)
CS 381 • Typing
11
CS 381 • Typing
12
Example: Expression Language with 2 Types
Expr2.hs
Type Safety
A programming language is called type safe if all type errors are detected
Type Safety
Type Safe Languages
Lisp (ridiculous type system) Java
Haskell
Expr + eval
Expr + evalDynTC CS 381 • Typing
Unsafe Languages (type casts, pointers)
C
C++
JavaScript (“foo” * 4 = NaN)
13
Exercises (1) Implement an unsafe eval function
for the language Expr
(a) Use Int as the semantic domain (b) Map boolean values to 0 and 1
(2) Evaluate unsafe expressions CS 381 • Typing
Expr2Unsafe.hs
data Expr = N Int
| Plus Expr Expr
| Equal Expr Expr
| Not Expr
14
Strong vs.Weak Typing
Strong Typing
Each value has one precisely determined type
Weak Typing
Values can be interpreted in different types (e.g.“17” can be used as a string or number, or 0 can be used as a number or boolean)
In practice: Only strongly typed languages are safe (although strong typing does not guarantee safety)
CS 381 • Typing
15
CS 381 • Typing
16
A Type Checker for the Expression Language
Expr2.hs TypeCheck.hs
CS 381 • Typing
17
Dynamic vs. Static Typing
Dynamic Typing
Types are checked during runtime
Static Typing
Types and type errors are found during compile time
Statically Typed
Haskell
(Java)
Expr + evalStatTC
Dynamically Typed
Lisp Python
Expr + evalDynTC
StaticTyping is Conservative What is the type of the following expression?
if 3>4 then “hello” else 17 How about:
Under dynamic typing: Int Under static typing: type error
CS 381 • Typing
Under static typing: type error
18
f x = if test x then x+1 else False
Under dynamic typing: ?
Exercises
(1) What is the type of the following function under static and dynamic typing?
f x = if not x then x+1 else x (2) What is the type of the following function
under static and dynamic typing?
f x = f (x+1) * 2
CS 381 • Typing
19
CS 381 • Typing
20
Zoom Poll
Type Checking
Undecidability of Static Typing
test :: Int -> Bool
f x = if test x then x+1 else not x
f is type correct if test x yields True
f contains a type error if test x yields False
Since test x might not terminate, we cannot determinate the value statically, because of the undecidability of the halting problem.
CS 381 • Typing
21
Static typing approximates by assuming a type error when type correctness cannot be shown
Advantages & Disadvantages of Static/Dynamic Typing
Advantage
Disadvantage
Static Typing
prevents type errors
smaller & faster code early error detection (saves debugging)
rejects some o.k. programs
Dynamic Typing
detects type errors
fewer programming restrictions
faster compilation (& development?)
no guarantees
slower execution released programs may stop unexpectedly with type errors
CS 381 • Typing
22
CS 381 • Typing
23
A Type Checker for Arithmetic Language with Pairs
ExprPair.hs ExprNPair.hs
Haskell as a Mathematical Metalanguage
Grammars
(Languages)
2 Syntax
Data Types
Math World
(Semantic domains)
Functions
(Semantics)
3 Semantics
Functions
Sets
Data Types
Haskell World
CS 381 • Typing
= Executable Math World
24
Haskell as a Mathematical
Metalanguage
Math World
Grammars
(Languages)
2 Syntax
Data Types
Functions
(Typing)
Grammars
(Types)
4 Types
Functions
Data Types Haskell World
CS 381 • Typing
Typing = Static Semantics Semantics = Dynamic Semantics
25
Polymorphism
A value (function, method, …) is polymorphic if it has more than one type
Different forms of polymorphism can be distinguished based on: (a) relationship between types
(b) implementation of functions
CS 381 • Typing
26
CS 381 • Typing
27
Forms of Polymorphism
Parametric Polymorphism
(a) All types match a common “type pattern”
(b) One implementation, i.e., there is only one function
Ad Hoc Polymorphism (aka Overloading)
(a) Types are unrelated
(b) Implementationdiffersforeachtype,i.e.,different
functions are referred to by the same name
Subtype Polymorphism
(a) Types are related by a subtype relation
(b) One implementation (methods can be applied to objects of any subtype)
CS 381 • Typing
28
Parametric Polymorphism Haskell demo