TypeLang: a language with types
April 7, 2021
COM S 342 Principles of Programming Languages @ Iowa State University 1
Overview
Concepts Types
Type system
Type inference and type checking
Typelang (ML: LISP with types) Type rules (type checking rules)
COM S 342 Principles of Programming Languages @ Iowa State University 2
Why do we need types?
(define f (λ (x y) (y x)))
Which of the following will throw a dynamic error? (f 2 3) // throw a dynamic error
(f2(λ(x)(+1x)))
(f ‘2’ (λ (x) (+ 1 x)) // throw a dynamic error
COM S 342 Principles of Programming Languages @ Iowa State University 3
What is Type
Type is a property of program constructs such as variables and expressions
Divide program values into kinds: it defines a set of values (range of variables) and a set of operations on those values
Classes in OO languages define new types
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
Contract between producer and consumer regarding what values to expect
Procedure: e.g., parameter should be a function
Client that calls the procedure needs to follow this ”contact”
Specification
Ultra lightweight: type
Lightweight annotations: JML
Full mathematical formalism: Z, alloy
COM S 342 Principles of Programming Languages @ Iowa State University 5
Why Types
Abstraction:
think in terms of a group of values
Verification:
are we applying the operations correctly? report as compiler warnings
Documentation:
this input parameter only can be integers
Performance:
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
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
Java: statically typed languages, every variable name is bound both
to a type (at compile time, by means of a data declaration) to an object.
COM S 342 Principles of Programming Languages @ Iowa State University 9
Typed Languages
Python: dynamically typed languages
In a dynamically typed language, every variable name is (unless it is
null) bound only to an object.
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
Static vs dynamic types
Static: the type inferred at compile time Dynamic: the type inferred at run-time
Sound static typing
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
A language type system specifies which operations are valid for which types
Prevent execution errors
Determine whether programs are well behaved
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)
Type rules are defined on the structure of expressions
Type rules are language specific
COM S 342 Principles of Programming Languages @ Iowa State University 12
Type Systems
Decidably verifiable
There exists a type-checking algorithm to automatically ensure that
a program is well behaved
Transparent
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
Type rule, typing rule, type checking rules The typing rules use very concise notation They are very carefully constructed
Virtually any change in a rule either:
Makes the type system unsound (bad programs are accepted as well typed)
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
We say a type system is sound if well-typed programs are well behaved (free of execution errors)
It is a property of the type system
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
Type Checking is the process of verifying fully typed programs
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
Type Checking
Static checking process to prevent unsafe and ill behaved program
from ever running
Check if the program confirms to the type rules
Type Checker
Algorithm or a tool that performs type checking
Ill typed program
program has a type error – errors in the code that violates the type
rules
Well typed program
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
Type checking can disallow execution (similar to compile time errors)
Type checking can block execution (similar to run time errors)
Dynamic checking?
Enforce good behavior by performing run time checks to rule out
forbidden errors Example: LISP
COM S 342 Principles of Programming Languages @ Iowa State University 18
Design Decisions for Types
Should languages be typed? 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
Should languages be type safe?
“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
Should languages be safe (strongly typed languange)?
No in reality
C is deliberately unsafe
Run time checks are too expensive 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
Grammar
Adding type declarations for firstly introduced values/variables
Let expression
Define expression
Lambda expression List expressions
RefLang expressions
Type checking rules
COM S 342 Principles of Programming Languages @ Iowa State University 23
TypeLang: T
Base type
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
Type for this function is, num num num − > num
Declares the same function and also calls it by passing integer parameters 1, 2 and 3 for arguments x, y and z
Type checks!
COM S 342 Principles of Programming Languages @ Iowa State University
27
Typing λ-function and calls
Won’t typecheck
#tisofbooltypenotanumtype
COM S 342 Principles of Programming Languages @ Iowa State University 28
Typing Refs
refexp : ‘(’ ‘ref’ ‘:’ T exp ‘)’ (ref : num 2)
Allocates a memory location of type number with value 2
(ref: Refnum(ref: num2))
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
(let (
(r: RefRefnum(ref: Refnum(ref: num5))) )
(deref (deref r)) )
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
listexp : ‘(’ ‘list’ ‘:’ T exp∗ ‘)’ Examples
(list: num123)
Constructs a list with elements 1, 2 and 3 of type number. Typechecks?
(list: num12#t) Typechecks?
COM S 342 Principles of Programming Languages @ Iowa State University 31
Typing Pair and List
More examples
(null? (cons 1 2)) Typechecks?
(cons 1 2) : constructs a pair type (num, num) (list : List
Typechecks?
(list : List
Typechecks?
COM S 342 Principles of Programming Languages @ Iowa State University 32
Typing Pair and List
For a pair expression, do the types for the first and second element has to be same?
No.
Example Scripts:
COM S 342 Principles of Programming Languages @ Iowa State University 33
Typing Pair and List
How about a list where elements are pairs?
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
$ (define pi : num 3.14159265359)
$ (define r : Ref num(ref : num 2))
$ (define u : unit (free (ref : num 2)))
$ (define iden : (num − > num) (lambda (x : num) x))
$(defineid: (num−>num)(lambda(x: (num−>num))x)) //incorrect
$ (define fi : num “Hello”) //incorrect
$ (define f : Ref num(ref : bool #f)) //incorrect
$ (define t : unit (free (ref : bool #t)))
COM S 342 Principles of Programming Languages @ Iowa State University 35
Typing Checking Rule
Logical rules about types
Assert a Fact (Fact A)
A
Imply: conditional assertion
COM S 342 Principles of Programming Languages @ Iowa State University 36
TypeChecking Rules for Constant
TypeLang assert that all numeric values (constants) have type num Notation:
(Num) n : num
Parts:
Name of the rules
Before ‘:’ expression or program After ‘:’ type
Reads: n has a type of num
COM S 342 Principles of Programming Languages @ Iowa State University 37
TypeChecking Rules for Constant
TypeLang assert that all Boolean values (constants) have type bool Notation:
(Num) n : bool
Reads: n has a type of bool
COM S 342 Principles of Programming Languages @ Iowa State University 38
Type Checking Rules for Atomic Expressions
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
Typing environment (or type environment)
tenv |− e:T should be read as assuming the type environment tenv,
the expression e has type t
A record of the types of variables during the processing of program fragments
In compiler it is just a symbol table
COM S 342 Principles of Programming Languages @ Iowa State University 40
Type Environment
Value environment (in Varlang)
What should be the value of a variable x?
Similarly, type environment
What should be the type of a variable?
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
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.
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
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).
It also clearly states the conditions under which the addition expression is going to produce a numerical value.
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
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
What should be the type of a variable expression x?
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
type environment used to perform typechecking of subexpressions is the same as that of the addition expression
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
Body (consumer of parameter values and producer of the result value)
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
Type for this function is, num num num − > num
Declares the same function and also calls it by passing integer parameters 1, 2 and 3 for arguments x, y and z
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
Concepts
Typelang: introduce types for different types of expressions Syntax
Semantics: Type Checking Rules: examples, formal notations Further Reading: Rajan’s Chapter 10, Sebester Chapter 6
COM S 342 Principles of Programming Languages @ Iowa State University 56