I. overview of semantics (Schmidt's: The structure of typed Prog Langs) A. introduction (preface) ------------------------------------------ STRUCTURE OF TYPED PROG LANGS Goals: - structuring techniques - design principles - role of type theory CONNECTION OF LANGUAGE AND LOGIC (CURRY-HOWARD ISOMORPHISM) language logic type system ~ propositions programs Examples: ------------------------------------------ B. outline ------------------------------------------ OUTLINE 1: core language (data, ops, control) tools: abstract syntax, type checking laws (rules) denotational semantics 2. Abstraction principle (naming, declarations) explains: procedures, functions, consts, modules, classes evaluation strategies how variable decls affect language. 3. Parameterization principle explains: parameter transmission Correspondence principle (how should declarations relate to parameters) 4. qualification principle (encapsulation) explains: scope, extent, encapsulation, objects, subtyping, inheritance 5. summary and consolidation ------------------------------------------ II. core imperative language (Schmidt 1.1) ------------------------------------------ CORE OF A PROGRAMMING LANGUAGE def: the *core* of a programming language Examples: ------------------------------------------ What's the core of Haskell? C? What's the goal in designing the core for a general purpose language? ------------------------------------------ SCHMIDT'S DESIGN METHOD 1. Start with 2. ------------------------------------------ A. core imperative language (1.1) 1. abstract syntax ------------------------------------------ CORE IMPERATIVE LANGUAGE (1.1) (While0) Abstract Syntax: C \in Command E \in Expression L \in Location N \in Numeral C ::= L := E | skip | C1 ; C2 | if E then C1 else C2 fi | while E do C od E ::= N | @L | E1 + E2 | not E | E1 = E2 L ::= loc , if i > 0 i N ::= n, if n \in Integer Examples: ------------------------------------------ Why separate a language into different syntactic domains? Can you give some examples? How would you model this in Haskell? ------------------------------------------ HASKELL MODEL OF SYNTAX type C = data Command = data Location = Loc Integer type Numeral = Integer Examples: ------------------------------------------ Can you give the examples in the Haskell notation? What are the differences between the Haskell and the standard notation? 2. abstract vs. concrete syntax ------------------------------------------ ABSTRACT vs. CONCRETE SYNTAX def: *abstract syntax* describes def: *concrete syntax* describes ------------------------------------------ III. typing rules (Schmidt 1.2) A. why? does the abstract syntax completely define legality? B. type attributes What kind of grammar are we using for abstract syntax? What kind of grammar do we need to exclude nonsense? ------------------------------------------ TYPE ATTRIBUTES (following Reynolds) type attribute use int intloc intexp, boolexp comm ------------------------------------------ ------------------------------------------ KINDS OF SYNTAX TREES abstract syntax tree: C / \ L := E (Loc 1) | N 0 attributed syntax tree: C: terminology: type annotation, type attribute well formed, well typed attributed syntax tree ------------------------------------------ C. typing rules how should we go about defining how to attach type attributes to a program? ------------------------------------------ TYPING RULES What rule for N ::= n, if n \in Integer? Examples: What rule for E ::= N? Examples: ------------------------------------------ What would you do for L ::= loci ? What would you do for E ::= @L ? What would you do for E ::= E1 + E2 ? ------------------------------------------ MORE TYPING RULES What rule for C ::= L := E? Example: ------------------------------------------ What would you do for C ::= if E then C1 else C2 fi ? ------------------------------------------ ATTACHING TYPE ATTRIBUTES while 0 = 0 do loc5 := @loc4 + 1 od ------------------------------------------ D. modeling type rules in Haskell ------------------------------------------ MODELING ATTRIBUTES IN HASKELL > data TypeAttrib = Aint | Abool > | Aintloc > | Aexp TypeAttrib > | Acomm deriving Eq > data AttribTree syntax attrib = > syntax ::: attrib > type ATree syntax = > AttribTree syntax TypeAttrib > infixr `ASemi` > type AC = ACommand > type AE = AExpression > type AL = ALocation > type AN = ANumeral > type ACommand = ATree Command' > data Command' = ASkip | AL `AAssign` AE > | AC `ASemi` AC > | AIf AE AC AC > | AWhile AE AC > type AExpression = ATree Expression' > data Expression' = ANum AN | ADeref AL > | AE `APlus` AE > | ANot AE | AE `AEquals` AE > type ALocation = ATree Location > type ANumeral = ATree Numeral ------------------------------------------ Why don't we just use AExpression = ATree Expression? ------------------------------------------ EXAMPLES OF ANNOTATION ? annotateN 7 ? annotateL (Loc 541) ? annotateE (Deref (Loc 541)) ? annotateE (Num 541) ? annotateE ((Num 541) `Plus` (Num 342)) APlus (ANum (541 ::: Aint) ::: Aexp Aint) (ANum (342 ::: Aint) ::: Aexp Aint) ::: Aexp Aint ? annotateE ((Num 3) `Equals` (Num 4)) AEquals (ANum (3 ::: Aint) ::: Aexp Aint) (ANum (4 ::: Aint) ::: Aexp Aint) ::: Aexp Abool ? annotateC ((Loc 1) `Assign` (Num 541)) AAssign (Loc 1 ::: Aintloc) (ANum (541 ::: Aint) ::: Aexp Aint) ::: Acomm ? annotateC ((Loc 3) `Assign` ((Num 3) `Equals` (Num 4))) Program error: {v718 (Loc 3 ::: Aintloc,.. ------------------------------------------ ------------------------------------------ MODELING THE TYPE RULES > annotateC :: Command -> ACommand > annotateC (l `Assign` e) = > (case (annotateL l, annotateE e) of > (al@(_::: Aintloc), > ae@(_::: Aexp Aint)) -> > (al `AAssign` ae) ::: Acomm) > annotateC Skip = ------------------------------------------ Can you write the other cases? ------------------------------------------ TYPING RULES FOR EXPRESSIONS > annotateE (Deref l) = > (case (annotateL l) of > al@(_:::Aintloc) -> > (ADeref al):::Aexp Aint) > annotateE (Num n) = > (case (annotateN n) of > an@(_:::Aint) -> > (ANum an):::Aexp Aint) > annotateE (e1 `Plus` e2) = > (case (annotateE e1, annotateE e2) of > (ae1@(_:::Aexp Aint), > ae2@(_:::Aexp Aint)) -> > (ae1 `APlus` ae2):::Aexp Aint) > annotateE (Not e) = > (case (annotateE e) of > ae@(_:::Aexp Abool) -> > (ANot ae):::Aexp Abool) > annotateE (e1 `Equals` e2) = > (case (annotateE e1, annotateE e2) of > (ae1@(_:::Aexp at1), > ae2@(_:::Aexp at2)) > | at1 == at2 -> > (ae1 `AEquals` ae2):::Aexp Abool) ------------------------------------------ ------------------------------------------ REMAINING RULES > annotateL :: Location -> ALocation > annotateL (Loc i) | i > 0 = > (Loc i):::Aintloc > annotateN :: Numeral -> ANumeral > annotateN n = n:::Aint ------------------------------------------ E. terms ------------------------------------------ TERMINOLOGY type assertion, type judgement U : t static typing, dynamic typing def: a language is *strongly typed* iff Questions: unicity of typing soundness ------------------------------------------ F. induction and recursion (1.3) G. unicity of typing (1.4) How would we prove that for every phrase P, if P:t holds, then t is unique? H. typing rules define the language (1.5) ------------------------------------------ TYPING RULES DEFINE THE LANGUAGE (1.5) !--------------------------------------! ! strings of tokens ! ! !----------------------------------! ! ! ! abstract syntax trees ! ! ! ! !------------------------------! ! ! ! ! ! type annotated trees ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !------------------------------! ! ! ! !----------------------------------! ! !--------------------------------------! AXIOMS AND RULES DEFINE A LOGIC !--------------------------------------! ! strings of symbols ! ! !----------------------------------! ! ! ! well-formed formulas ! ! ! ! !------------------------------! ! ! ! ! ! provable formulas ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !------------------------------! ! ! ! !----------------------------------! ! !--------------------------------------! ------------------------------------------ What's this like in compilers? ------------------------------------------ TYPE RULES AS RULES OF LOGIC Axioms: n:int, if n \in Integer loc_i:intloc, if i > 0 Inference rules: N:int _______ N:intexp L:intloc E: intexp ___________________ (L := E): comm Proof tree: ------------------------------------------ So what's the annotated syntax tree in terms of the logic? Can there be more than one proof tree for a well-typed program in While0? I. non-unique typings and coherernce (skip) ------------------------------------------ NON UNIQUE TYPINGS Suppose we add these rules: E: intexp E1: realexp E2: realexp _________ ________________________ E: realexp E1+E2 : realexp What proof trees are there for 5 + 4 : realexp? def: a type system is *coherent* if each derivation of E:t has ------------------------------------------ IV. semantics of the core language (Schmidt 1.6) A. denotational semantics ------------------------------------------ SEMANTICS semantics = meaning : annotated syntax trees -> answers e.g., meaning :: AExpression -> (DStore -> ExpressibleValue) SEMANTIC DEFINITION STYLES denotational style: operational style: "structural operational" style: axiomatic style: ------------------------------------------ ------------------------------------------ THE DENOTATIONAL APPROACH To define language semantics: a. define abstract syntax b. (optional) define type rules c. define domains (sets + operations) d. define functions from annotated syntax trees to domains - follows syntax - compositional = - referentially transparent = ------------------------------------------ Why is referential transparency a good idea in the specification of programming languages? B. semantic domains for core (Fig 1.6) ------------------------------------------ SEMANTIC DOMAINS MODELED IN HASKELL The booleans > type DBool = Bool > true = True > false = False > -- Operations: > -- not is already in Haskell > equalbool :: (DBool, DBool) -> DBool > equalbool(m, n) = (m == n) The integers > type DInt = Integer > -- Operations: > plus :: (DInt,DInt) -> DInt > plus(m,n) = m + n > equalint :: (DInt,DInt) -> DBool > equalint(m,n) = (m == n) Locations > -- recall: data Location = Loc Integer > type DLocation = Location ------------------------------------------ How many DBool values are there? ------------------------------------------ MODELING STORES IN HASKELL Stores > type DStore = [DInt] > -- Operations: > lookup :: (DLocation,DStore) -> DInt > update :: (DLocation,DInt,DStore) > -> DStore > -- if is already in Haskell ------------------------------------------ C. semantic functions Now how do we go about defining the meaning of each annotated syntax tree? ------------------------------------------ SEMANTIC FUNCTIONS > meaningN :: ANumeral -> DInt > meaningN ((n ::: Aint)) = n > meaningL :: ALocation -> DLocation > meaningL (((Loc i) ::: Aintloc)) = ------------------------------------------ ------------------------------------------ MEANINGS FOR EXPRESSIONS meaningE :: AExpression -> ------------------------------------------ ------------------------------------------ EXAMPLES OF EXPPRESSION MEANINGS ? meaningE (annotateE (Num 7)) [] ? meaningE (annotateE (Deref (Loc 1))) [3] ? meaningE (annotateE ((Num 3) `Equals` (Num 4))) [] > evalE = meaningE . annotateE ? evalE (Num 3) [] InInt 3 ------------------------------------------ What happens if we leave off the store argument? ------------------------------------------ EXAMPLES OF COMMAND MEANINGS > evalC = meaningC . annotateC ? evalC Skip [] ? evalC ((Loc 1) `Assign` (Num 4)) [7] ? evalC (((Loc 1) `Assign` (Num 4)) `Semi` ((Loc 1) `Assign` ((Deref (Loc 1)) `Plus` (Deref (Loc 1))))) [3] ------------------------------------------ ------------------------------------------ MEANINGS FOR COMMANDS > meaningC :: ACommand -> DStore -> DStore > meaningC ((ASkip ::: Acomm)) s = s > meaningC (((al `AAssign` > ae@(_:::Aexp Aint)) > ::: Acomm)) s = > (case meaningE((ae)) s of > (InInt i) -> > update(meaningL(al), i, s)) > meaningC (((ac1 `ASemi` ac2) ::: Acomm)) > s = > meaningC((ac2)) (meaningC((ac1)) s) > meaningC (((AIf ae@(_:::Aexp Abool) > ac1 ac2) ::: Acomm)) s = > (case meaningE((ae)) s of > (InBool b) -> > if b then meaningC((ac1)) s > else meaningC((ac2)) s) > meaningC (((AWhile ae@(_:::Aexp Abool) > ac) ::: Acomm)) s = > w(s) > where w s' = > (case meaningE ae s' of > (InBool b) -> > if b > then w(meaningC((ac)) s') > else s') ------------------------------------------ What's strange about this definition of while loops? ------------------------------------------ MEANING OF RECURSIVELY DEFINED FUNCTION w_0(s) = _ w_1(s) = if([[E: boolexp]](s), w_0([[C: comm]](s)), s) w_2(s) = if([[E: boolexp]](s), w_1([[C: comm]](s)), s) ... terminology: proper meaning improper meaning def: a function, f, is *strict* iff ------------------------------------------ Is meaningC a strict function as written in Haskell? Given that Haskell has an operator strict :: (a -> b) -> (a -> b) How would you make meaningC strict? D. using the semantics ------------------------------------------ CALCULATING THE MEANING OF A PHRASE [[loc_3 := @loc_3 + 1: comm]]([5,4,0]) = ------------------------------------------ E. summary What's the use of this semantics? V. soundness of the typing rules (1.7) ------------------------------------------ SOUNDNESS OF THE TYPING RULES (1.7) Soundness means: Formalizing this: ------------------------------------------ ------------------------------------------ MEANINGS FOR TYPES Attributes: tau ::= int | bool theta ::= intloc | tau exp | comm Meanings for type attributes: [[int]] = Int [[bool]] = Bool [[intloc]] = Location [[tau exp]] = Store -> [[tau]] [[comm]] = Store -> Store _|_ ------------------------------------------ What are some examples of theta? ------------------------------------------ SOUNDNESS THEOREM FOR TYPE RULES Thm: For all well-typed phrases, P: theta, [[P:theta]] \in [[theta]] ------------------------------------------ How does the proof go? VI. operational properties of semantics (1.8) A. what is it? ------------------------------------------ OPERATIONAL SEMANTICS Shows computation steps taken by a program Good for: - modeling compiled code - studying efficiency issues Not so good for: - studying program equivalence ------------------------------------------ B. subtree replacement systems 1. example ------------------------------------------ USING DENOTATIONAL SEMANTICS AS AN OPERATIONAL SEMANTICS [[loc_3 := @loc_3 + 1: comm]]([5,4,0]) ==> update([[loc_3:intloc]], [[@loc_3+1:intexp]]([5,4,0]), [5,4,0]) ==> ------------------------------------------ 2. formalizing this idea ------------------------------------------ SUBTREE REPLACEMENT SYSTEMS Work on texts (phrases). Identify set of Values (answers): Bool values = {true, false} Int values = { ..., -1, 0, 1, ...} Not values: not(false), plus(1,2) Orient equations from left to right: [[skip: comm]](s) ==> s [[n: int]] ==> n def: a subphrase f(e1,...,en) is a *redex* if computation step: replace redex by rhs in the phrase, written p0 ==> p1 computation: a sequence p0 ==> p1 ==> ... ==> pn i.e., p0 ==>* pn ------------------------------------------ WHen would you say a computation *terminates*? 3. properties ------------------------------------------ PROPERTIES OF SUBTREE REPLACEMENT SYSTEMS Subject reduction: Soundness: Strong typing: Computational adequacy: ------------------------------------------ do these hold? why? when? VII. design of a language core (1.9) ------------------------------------------ DESIGN OF A LANGUAGE CORE (1.9) Goals: - works well in some problem area - security - orthogonality - simple etc. Denotational method: - pick sets of meanings - design operations - give syntax to meanings and ops, using an abstract syntax - design ------------------------------------------ How is this method reflected in the While0 core design? Why have type attributes and typing rules? Does if have to be limited to working on stores?