TypeLang: a language with types
TypeLang: a language with types
April 7, 2021
COM S 342 Principles of Programming Languages @ Iowa State University 1
Overview
I Concepts
I Types
I Type system
I Type inference and type checking
I Typelang (ML: LISP with types)
I Type rules (type checking rules)
COM S 342 Principles of Programming Languages @ Iowa State University 2
Why do we need types?
I (define f (λ (x y) (y x)))
I Which of the following will throw a dynamic error?
I (f 2 3) // throw a dynamic error
I (f 2 (λ (x) (+ 1 x)))
I (f ‘2’ (λ (x) (+ 1 x)) // throw a dynamic error
COM S 342 Principles of Programming Languages @ Iowa State University 3
What is Type
I Type is a property of program constructs such as variables and
expressions
I Divide program values into kinds: it defines a set of values (range of
variables) and a set of operations on those values
I Classes in OO languages define new types
I fields and methods of a Java class are meant to correspond to values
and operations
COM S 342 Principles of Programming Languages @ Iowa State University 4
Type as a Contract or Specification
I Contract between producer and consumer regarding what values to
expect
I Procedure: e.g., parameter should be a function
I Client that calls the procedure needs to follow this ”contact”
I Specification
I Ultra lightweight: type
I Lightweight annotations: JML
I Full mathematical formalism: Z, alloy
COM S 342 Principles of Programming Languages @ Iowa State University 5
Why Types
I Abstraction:
I think in terms of a group of values
I Verification:
I are we applying the operations correctly?
I report as compiler warnings
I Documentation:
I this input parameter only can be integers
I Performance:
I language implementation optimize for types
COM S 342 Principles of Programming Languages @ Iowa State University 6
COM S 342 Principles of Programming Languages @ Iowa State University 7
Typed Languages
I A language is typed: association between expressions are valid
only when the types match; Otherwise, the language is not (weakly)
typed.
Figure: Example for not(weakly) typed language
Figure: Example for strongly typed language
COM S 342 Principles of Programming Languages @ Iowa State University 8
Typed Languages
I Java: statically typed languages, every variable name is bound
both
I to a type (at compile time, by means of a data declaration)
I to an object.
COM S 342 Principles of Programming Languages @ Iowa State University 9
Typed Languages
I Python: dynamically typed languages
I In a dynamically typed language, every variable name is (unless it is
null) bound only to an object.
I Names are bound to objects at execution time by means of
assignment statements, and it is possible to bind a name to objects
of different types during the execution of the program.
COM S 342 Principles of Programming Languages @ Iowa State University 10
Static and dynamic types
I Static vs dynamic types
I Static: the type inferred at compile time
I Dynamic: the type inferred at run-time
I Sound static typing
I Static: Dynamic type of an entity is a subset of Static type of the
entity
COM S 342 Principles of Programming Languages @ Iowa State University 11
Type Systems and Type Rules
I A language type system specifies which operations are valid for
which types
I Prevent execution errors
I Determine whether programs are well behaved
I A type system is a collection of rules that assign types to program
constructs (more constraints added to checking the validity of the
programs, violation of such constraints indicate errors)
I Type rules are defined on the structure of expressions
I Type rules are language specific
COM S 342 Principles of Programming Languages @ Iowa State University 12
Type Systems
I Decidably verifiable
I There exists a type-checking algorithm to automatically ensure that
a program is well behaved
I Transparent
I Programmer should be able to predict easily whether a program will
correctly type-check
COM S 342 Principles of Programming Languages @ Iowa State University 13
Typing Rules
I Type rule, typing rule, type checking rules
I The typing rules use very concise notation
I They are very carefully constructed
I Virtually any change in a rule either:
I Makes the type system unsound (bad programs are accepted as well
typed)
I Makes the type system less usable (perfectly good programs are
rejected)
COM S 342 Principles of Programming Languages @ Iowa State University 14
Type System Soundness
I We say a type system is sound if well-typed programs are well
behaved (free of execution errors)
I It is a property of the type system
I There can be many sound type rules, we need to use the most
precise ones so it can be useful
COM S 342 Principles of Programming Languages @ Iowa State University 15
Type Checking and Type Inferences
I Type Checking is the process of verifying fully typed programs
I Type Inference is the process of filling in missing type information
COM S 342 Principles of Programming Languages @ Iowa State University 16
Type Checking and Type Inferences
I Type Checking
I Static checking process to prevent unsafe and ill behaved program
from ever running
I Check if the program confirms to the type rules
I Type Checker
I Algorithm or a tool that performs type checking
I Ill typed program
I program has a type error – errors in the code that violates the type
rules
I Well typed program
I program has no type error and will pass the typechecker
COM S 342 Principles of Programming Languages @ Iowa State University 17
Static Type Checking and Dynamic Type Checking
I Type checking can disallow execution (similar to compile time
errors)
I Type checking can block execution (similar to run time errors)
I Dynamic checking?
I Enforce good behavior by performing run time checks to rule out
forbidden errors
I Example: LISP
COM S 342 Principles of Programming Languages @ Iowa State University 18
Design Decisions for Types
I Should languages be typed?
I Debatable
COM S 342 Principles of Programming Languages @ Iowa State University 19
COM S 342 Principles of Programming Languages @ Iowa State University 20
Design Decisions for Types
I Should languages be type safe?
I “Type safe” usually refers to languages that ensure that an operation
is working on the right kind of data at some point before the
operation is actually performed. This may be at compile time or at
run time.
COM S 342 Principles of Programming Languages @ Iowa State University 21
Design Decisions for Types
I Should languages be safe (strongly typed languange)?
I No in reality
I C is deliberately unsafe
I Run time checks are too expensive
I Static analysis cannot always ensure
In assembler and C you can often treat a pointer as an integer, an
integer as a string, a 2-byte integer as a 4-byte integer, or series of
bytes as a structure. Used correctly, this can offer some
performance benefit because data doesn’t have to be copied or
translated if it can be“re-interpreted” as a different type.
COM S 342 Principles of Programming Languages @ Iowa State University 22
TypeLang
I Grammar
I Adding type declarations for firstly introduced values/variables
I Let expression
I Define expression
I Lambda expression
I List expressions
I RefLang expressions
I Type checking rules
COM S 342 Principles of Programming Languages @ Iowa State University 23
TypeLang: T
I Base type
I Recursively-defined types, i.e. their definition makes use of other
types
COM S 342 Principles of Programming Languages @ Iowa State University 24
Typing “Define”
COM S 342 Principles of Programming Languages @ Iowa State University 25
Typing LetExp
COM S 342 Principles of Programming Languages @ Iowa State University 26
Typing λ-function and calls
I Type for this function is,
num num num − > num
I Declares the same function
and also calls it by passing
integer parameters 1, 2 and
3 for arguments x , y and z
I Type checks!
COM S 342 Principles of Programming Languages @ Iowa State University 27
Typing λ-function and calls
I Won’t typecheck
I #t is of bool type not a num type
COM S 342 Principles of Programming Languages @ Iowa State University 28
Typing Refs
I refexp : ‘(’ ‘ref’ ‘:’ T exp ‘)’
I (ref : num 2)
I Allocates a memory location of type number with value 2
I (ref : Ref num (ref : num 2))
I Allocates a memory location of type to a reference which its content
is 2.
COM S 342 Principles of Programming Languages @ Iowa State University 29
Typing Refs
I (let
(
(r : Ref Ref num (ref : Ref num (ref : num 5)))
)
(deref (deref r))
)
I Declares r as reference to a reference with value number 5 and
evaluation of the program returns 5
COM S 342 Principles of Programming Languages @ Iowa State University 30
Typing Pair and List
I listexp : ‘(’ ‘list’ ‘:’ T exp∗ ‘)’
I Examples
I (list : num 1 2 3)
I Constructs a list with elements 1, 2 and 3 of type number.
I Typechecks?
I (list : num 1 2 #t)
I Typechecks?
COM S 342 Principles of Programming Languages @ Iowa State University 31
Typing Pair and List
I More examples
I (null? (cons 1 2))
I Typechecks?
I (cons 1 2) : constructs a pair type (num, num)
I (list : List
I Typechecks?
I (list : List
I Typechecks?
COM S 342 Principles of Programming Languages @ Iowa State University 32
Typing Pair and List
I For a pair expression, do the types for the first and second element
has to be same?
I No.
Example Scripts:
COM S 342 Principles of Programming Languages @ Iowa State University 33
Typing Pair and List
I How about a list where elements are pairs?
I Recall, that elements of the list has to be of the same type.
Example Scripts:
COM S 342 Principles of Programming Languages @ Iowa State University 34
More Examples of Typelang
I $ (define pi : num 3.14159265359)
I $ (define r : Ref num(ref : num 2))
I $ (define u : unit (free (ref : num 2)))
I $ (define iden : (num − > num) (lambda (x : num) x))
I $ (define id : (num − > num) (lambda (x : (num − > num)) x))
//incorrect
I $ (define fi : num “Hello”) //incorrect
I $ (define f : Ref num(ref : bool #f)) //incorrect
I $ (define t : unit (free (ref : bool #t)))
COM S 342 Principles of Programming Languages @ Iowa State University 35
Typing Checking Rule
I Logical rules about types
I Assert a Fact
(Fact A)
A
I Imply: conditional assertion
COM S 342 Principles of Programming Languages @ Iowa State University 36
TypeChecking Rules for Constant
I TypeLang assert that all numeric values (constants) have type num
I Notation:
(Num)
n : num
I Parts:
I Name of the rules
I Before ‘:’ expression or program
I After ‘:’ type
I Reads: n has a type of num
COM S 342 Principles of Programming Languages @ Iowa State University 37
TypeChecking Rules for Constant
I TypeLang assert that all Boolean values (constants) have type bool
I Notation:
(Num)
n : bool
I Reads: n has a type of bool
COM S 342 Principles of Programming Languages @ Iowa State University 38
Type Checking Rules for Atomic Expressions
I Atomic: no subexpressions
(NumExp)
(NumExp n) : num
Producer: produce the expression – promise to produce type num
Consumer: use this expression – expect type num
COM S 342 Principles of Programming Languages @ Iowa State University 39
Type Environment
I Typing environment (or type environment)
I tenv |− e:T should be read as assuming the type environment tenv,
the expression e has type t
I A record of the types of variables during the processing of program
fragments
I In compiler it is just a symbol table
COM S 342 Principles of Programming Languages @ Iowa State University 40
Type Environment
I Value environment (in Varlang)
I What should be the value of a variable x?
I Similarly, type environment
I What should be the type of a variable?
I Map that provides operation to lookup the type
COM S 342 Principles of Programming Languages @ Iowa State University 41
Type rule for constants
The type environment doesn’t play a major role because values produced
(and thus types) of these expressions are not dependent on the context.
COM S 342 Principles of Programming Languages @ Iowa State University 42
Type Checking for Compound Expressions
I Conditional assertion: if subexpressions of the addition expression
always produce values of type num, then the addition expression will
produce a value of type num.
I if subexpressions e0 to en have type num, then the expression
(AddExp e0, e1, . . . , en) will have type num as well
COM S 342 Principles of Programming Languages @ Iowa State University 43
Type Checking for Compound Expressions
I This typechecking rule establishes a contract between producers of
values in this context (expressions e0, e1, . . . , en) and the consumer
of these values (the addition expression).
I It also clearly states the conditions under which the addition
expression is going to produce a numerical value.
I Note that the rule does not mention situations where expressions e0,
e1, . . . , en might produce a dynamic error. If expressions e0, e1, . . . ,
en fail to produce a numerical value the addition expression provides
no guarantees.
COM S 342 Principles of Programming Languages @ Iowa State University 44
Typing MultExp, SubExp, and DivExp
COM S 342 Principles of Programming Languages @ Iowa State University 45
Division Rethink
I This is an example of a situation where the type system being
developed is insufficient to detect and remove certain errors, i.e., the
divide-by-zero errors
COM S 342 Principles of Programming Languages @ Iowa State University 46
Variable Typing
I What should be the type of a variable expression x?
I What should be a typechecking rule for a variable expression?
COM S 342 Principles of Programming Languages @ Iowa State University 47
Type environment
COM S 342 Principles of Programming Languages @ Iowa State University 48
Type rule for VarExp
COM S 342 Principles of Programming Languages @ Iowa State University 49
Type rule for add expression
I type environment used to perform typechecking of subexpressions is
the same as that of the addition expression
I variables and their types stored in the type environment are not
affected by the addition expression
COM S 342 Principles of Programming Languages @ Iowa State University 50
Typing LetExp
Typelang requires that programmer specifies the types of identifiers in let
expression
COM S 342 Principles of Programming Languages @ Iowa State University 51
Type rules for LetExpr
COM S 342 Principles of Programming Languages @ Iowa State University 52
Typing λ-function and calls
I Body (consumer of parameter values and producer of the result
value)
I Caller (producers of parameter values and consumer of the result
value)
COM S 342 Principles of Programming Languages @ Iowa State University 53
Typing λ-function and calls
I Type for this function is,
num num num − > num
I Declares the same function
and also calls it by passing
integer parameters 1, 2 and
3 for arguments x , y and z
I Type checks!
COM S 342 Principles of Programming Languages @ Iowa State University 54
Typing λ-function and calls
COM S 342 Principles of Programming Languages @ Iowa State University 55
Summary
I Concepts
I Typelang: introduce types for different types of expressions
I Syntax
I Semantics: Type Checking Rules: examples, formal notations
I Further Reading: Rajan’s Chapter 10, Sebester Chapter 6
COM S 342 Principles of Programming Languages @ Iowa State University 56