Programming Languages andCompilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/fa06/cs421/Based in part on slides by Mattox Beckman, as updatedby Vikram Adve and Gul AghaElsa L. GunterWhy Data Types?• Data types play a key role in:– Data abstraction in the design of programs– Type checking in the analysis of programs– Compile-time code generation in thetranslation and execution of programsElsa L. GunterTerminology• Type: A type t defines a set ofpossible data values– E.g. short in C is {x| 215 - 1 ≥ x ≥ -215}– A value in this set is said to have typet• Type system: rules of a languageassigning types to expressionsElsa L. GunterTypes as Specifications• Types describe properties• Different type systems describe differentproperties, eg– Data is read-write versus read-only– Operation has authority to access data– Data came from “right” source– Operation might or could not raise an exception• Common type systems focus on types describingsame data layout and access methodsElsa L. GunterSound Type System• If an expression is assigned type t, andit evaluates to a value v, then v is in theset of values defined by t• SML, OCAML, Schema and Ada havesound type systems• Most implementations of C and C++ donotElsa L. GunterStrongly Typed Language• When no application of an operatorto arguments can lead to a run-timetype error, language is stronglytyped– Eg: 1 + 2.3;;• Depends on definition of “type”Elsa L. GunterStrongly Typed Language• C++ claimed to be “strongly typed”, but– Union types allow creating a value atone type and using it at another– Type coercions may causeunexpected (undesirable) effects– No array bounds check (in fact, noruntime checks at all)• SML, OCAML “strongly typed” but stillmust do dynamic array bounds checks,runtime type case analysis, and otherchecksElsa L. GunterStatic vs Dynamic Types• Static type: type assigned to anexpression at compile time• Dynamic type: type assigned to astorage location at run time• Statically typed language: static typeassigned to every expression at compiletime• Dynamically typed language: type of anexpression determined at run timeElsa L. GunterType Checking• When is op(arg1,…,argn) allowed?• Type checking assures that operationsare applied to the right number ofarguments of the right types– Right type may mean same type aswas specified, or may mean thatthere is a predefined implicit coercionthat will be applied• Used to resolve overloaded operationsElsa L. GunterType Checking• Type checking may be donestatically at compile time ordynamically at run time• Dynamically typed (aka untyped)languages (eg LISP, Prolog) doonly dynamic type checking• Statically typed languages can domost type checking staticallyElsa L. GunterDynamic Type Checking• Performed at run-time before eachoperation is applied• Types of variables and operationsleft unspecified until run-time– Same variable may be used atdifferent typesElsa L. GunterDynamic Type Checking• Data object must contain typeinformation• Errors aren’t detected until violatingapplication is executed (maybeyears after the code was written)Elsa L. GunterStatic Type Checking• Performed after parsing, beforecode generation• Type of every variable andsignature of every operator must beknown at compile timeElsa L. GunterStatic Type Checking• Can eliminate need to store typeinformation in data object if nodynamic type checking is needed• Catches many programming errorsat earliest point• Can’t check types that depend ondynamically computed values– Eg: array boundsElsa L. GunterStatic Type Checking• Typically places restrictions onlanguages– Garbage collection– References instead of pointers– All variables initialized when created– Variable only used at one type• Union types allow for work arounds, buteffectively introduce dynamic typechecksElsa L. GunterType Declarations• Type declarations: explicit assignmentof types to variables (signatures tofunctions) in the code of a program– Must be checked in a strongly typedlanguage– Often not necessary for strong typing oreven static typing (depends on the typesystem)Elsa L. GunterType Inference• Type inference: A program analysisto assign a type to an expressionfrom the program context of theexpression– Fully static type inference firstintroduced by Robin Miller in ML– Haskle, OCAML, SML all use typeinference• Records are a problem for typeinferenceElsa L. GunterFormat of Type Judgments• A type judgment has the form Γ |- exp : τ• Γ is a typing environment– Supplies the types of variables andfunctions– Γ is a list of the form [ x : σ , . . .]• exp is a program expression• τ is a type to be assigned to exp• |- pronounced “turnstyle”, or “entails” (or“satisfies”)Elsa L. GunterExample Valid TypeJudgments• [ ] |- true or false : bool• [ x : int] |- x + 3 : int• [ p : int -> string ] |- p(5) : stringElsa L. GunterFormat of Typing RulesAssumptions Γ1 |- exp1 : τ1 . . . Γn |- expn : τn Γ |- exp : τConclusion• Idea: Type of expression determined bytype of components• Rule without assumptions is called anaxiom• Γ may be omitted when not neededElsa L. GunterFormat of Typing RulesAssumptions Γ1 |- exp1 : τ1 . . . Γn |- expn : τn Γ |- exp : τConclusion• Γ, exp, τ are parameterizedenvironments, expressions and types -i.e. may contain meta-variablesElsa L. GunterAxioms - Constants|- n : int (assuming n is an integerconstant)|- true : bool |- false : bool• These rules are true with any typingenvironment• n is a meta-variableElsa L. GunterAxioms - VariablesNotation: Let Γ(x) = σ if x : σ ∈ Γ andthere is no x : τ to the left of x : σ in ΓVariable axiom: Γ |- x : σ if Γ (x) = σElsa L. GunterSimple Rules - ArithmeticPrimitive operators ( ⊕ ∈ { +, -, *, …}): Γ |- e1 : int Γ |- e2 : int Γ |- e1 ⊕ e2 : intRelations ( ˜ ∈ { < , > , =, <=, >= }):Γ |- e1 : int Γ |- e2 : int Γ |- e1 ˜ e2 :boolElsa L. GunterSimple Rules - BooleansConnectives Γ |- e1 : bool Γ |- e2 : bool Γ |- e1 && e2 : bool Γ |- e1 : bool Γ |- e2 : bool Γ |- e1 || e2 : boolElsa L. GunterSimple Example• Let Γ = [ x:int ; y:bool]• Show Γ |- y || (x + 3 > 6) : bool• Start building the proof tree from the bottom up? Γ |- y || (x + 3 > 6) : boolElsa L. GunterSimple Example• Let Γ = [ x:int ; y:bool]•
View Full Document
Unlocking...