CS计算机代考程序代写 algorithm python compiler Java assembler 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
􏰉 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 (list : num 2))
􏰉 Typechecks?
􏰉 (list : List (list : bool #t))
􏰉 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