CS计算机代考程序代写 python compiler Java assembler algorithm TypeLang: a language with types

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 (list : num 2))
I Typechecks?

I (list : List (list : bool #t))
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