I. the parameterization and correspondence principles (Schmidt 3) A. principles ------------------------------------------ PARAMETERIZATION AND CORRESPONDENCE PRINCIPLES (SCHMIDT 3) Parameterization: Phrases from any syntactic class should be Correspondence: Abstraction and parameterization mechanisms should Lambda abstraction: Allow prameterized phrases, i.e., lambda abstractions. ------------------------------------------ Why is correspondence a good thing? ------------------------------------------ TYPE RULES FOR PARAMETERIZATION (3.10) Syntax (schematic): D ::= ... | define I1 (I2: theta1) = U U ::= ... | invoke I(V) V ::= ... | I Type attributes: theta ::= ... | Typing rules: ------------------------------------------ ------------------------------------------ TYPE RULES FOR LAMBDA ABSTRACTION Syntax: D ::= ... | define I = A A ::= \I:theta . U U ::= ... | invoke I(V) V ::= I Typing rules: ------------------------------------------ ------------------------------------------ PARAMETERIZATION SEMANTICS OVERVIEW kind of semantics parameter lazy eager expression location numeral command declaration type struct. function, procedure,... ------------------------------------------ What do we mean by a lazy or eager semantics for parameters? Why should function parameters be lazily evaluated? II. Expression parameters (Schmidt 3.1-3.3) A. syntax of expression parameters to procedures (3.1) ------------------------------------------ EXPRESSION PARAMETERS TO PROCEDURES (3.1) Syntax: D ::= proc C ::= call I(E) Examples: var v: newint; proc p(i:int exp) = (v:=i; v:=i) in v := 1; call P(@v+1) FOR YOU TO DO Give the type checking rules ------------------------------------------ What is the type attribute of I1 in the type rule? B. semantics (3.2) ------------------------------------------ EAGER SEMANTICS (3.2) Meaning of type attributes [[ tau exp -> comm]] = Semantics of declarations: [[ Semantics of invocations: [[ Semantics of formal parameter references: [[ ------------------------------------------ Does this satisfy the correspondence principle? What if the actual parameter loops? ------------------------------------------ LAZY SEMANTICS Meaning of type attributes [[ tau exp -> comm]] = Semantics of declarations: [[ Semantics of invocations: [[ Semantics of formal parameter references: [[ ------------------------------------------ How does this work? What would be another way to define this? C. type soundness What's involved in trying to prove type soundness for the lazy semantics? for the eager semantics? D. copy rule for lazily-evaluated parameters (3.3) ------------------------------------------ COPY RULE FOR LAZILY-EVALUATED PARAMETERS (3.3) Idea ... define I1(I2:t) = U ... in ... invoke I1(V) ... ==> ... define I1 = \I2:t.U ... in ... invoke I1(V) ... ==> ... (\I2:t.U)(V) ... ==> ... [V/I2]U ... ------------------------------------------ 1. lambda abstractions ------------------------------------------ LAMBDA ABSTRACTIONS Recall: pi' |- U : t2 ____________________________________ pi |- \I:t1.U : t1 -> t2 where pi' = pi unionMinus {I:t1} Semantics: Parameter copy rule (beta reduction): ------------------------------------------ III. Other Varieties of parameters (Schmidt 3.4) Besides expression parameters, what other kinds might we have? ------------------------------------------ OTHER KINDS OF PARAMETERS (3.4) Command and numeral parameters: const K = 2; var A:newint; proc P(M:comm) = (A:=K+1; call M); proc Q(X:int) = A := X in call P(call Q(2)); call P(call P(call Q(K))); call P(A:= K) ------------------------------------------ What should the evaluation mechanism for numeral parameters be? What about command parameters? A. declaration parameters ------------------------------------------ DECLARATION PARAMETERS Can be useful in modules: module COUNTER(M:{X: int loc, INIT: comm} dec) = { import M; proc P = (call INIT; X := @X+1) } module N = {var X: newint; proc INIT = X := 0 } import COUNTER(import N) What I want in Haskell: module TypeHelpers(A:{attrib:...} dec) = { proc rule = ... }; module Attributes = {type attrib = ...}; import TypeHelpers(import Attributes); ------------------------------------------ What's a module with a declaration parameter like in ML? Do we need to have the argument to COUNTER in a module? Would declaration parameters be useful for other kinds of abstractions besides declaration abstractions (modules)? ------------------------------------------ VARIABLE PARAMETERS Simple ones: var A: newint; proc P(B:int loc) = A := @A + @B; var X:newint in A := 541; X := 641; P(X) Record variables: class K = record var A: newint; proc P(B:int loc) = A:=@A+@B end; var R: K; proc Q(Y: {A:int loc, P: int loc -> comm}) = call Y.P(Y.A) in R.A := 0; call Q(R) ------------------------------------------ What about P(3)? Should that be ok? Should we use lazy or eager semantics? Are they the same? The type of Y is wordy. Should we write Y:K? What else could we do? How should record types be compared? IV. type equivalence (3.5) A. the problem ------------------------------------------ TYPE EQUIVALENCE (3.5) How to check actual's type vs. formals? Example: class Car = record var age: newint, var weight: newint end; class Person = record var age: newint, var weight: newint end; class Ship = Car; var c: Car; var p: Person; var s: Ship; var c2: record var age: newint, var weight: newint end; var p2: record var age: newint, var weight: newint end; proc con(r: {age:intloc, weight:intloc}) = r.weight := r.weight + 1 ------------------------------------------ Which of the variables (if any) can be passed to con? B. structural and by-name equivalence ------------------------------------------ NOTIONS OF TYPE EQUIVALENCE structural: name (occurrence): ------------------------------------------ What rule is used in C for comparing types? In Java? What do C and C++ do with typedefs? What about Haskell data and type declarations? What kinds of parameter types are useful with occurrence equivalence? What are the advantages of occurrence equivalence? Disadvantages? C. typing rules ------------------------------------------ BY NAME TYPING RULES Schmidt's version: pi |- D: ___________________________ pi |- record D end: What are the types of our example? ------------------------------------------ Is that typing rule functional? D. leave it to the programmer to decide V. type structure parameters (3.6) ------------------------------------------ TYPE STRUCTURE PARAMETERS (3.6) var default : newint; class INTCELL = record var A: newint; proc INIT = A := 0 end; class DEFCELL = record var A: newint; proc INIT = A := @default end; class K(T:{A:int loc, INIT: comm} class) = record var S: T, proc GO = (default := 3; call S.INIT) end; var x: K(INTCELL); var y: K(DEFCELL) in x.S.A := 4; call y.GO ------------------------------------------ What's the right semantics for this: eager or lazy? VI. the correspondence principle (3.7) A. in negation ------------------------------------------ THE ANTI-CORRESPONDENCE PRINCIPLE You can make your language - harder to learn, and - less regular if the semantics of binding identifiers is Example: use lazy evaluation for functions, eager evaluation for exp parameters var a: newint; fun f = @a+1; proc p(x:int exp) = (a:=x+f; a:=x+f); in a := 0; call p(f) Counter-examples: ------------------------------------------ Can you tell from the form of x and f what kind of evaluation is used? How could that be fixed? B. disproof of correspondence (3.7.1) ------------------------------------------ PROVING LACK OF CORRESPONDENCE Example: expression parameters to procedures. Must show: for some e, s, E, I1, I2, C, such that I1 not in ({I2} U FV(E)) [[fun I2 = E in C]] e s =/= [[proc I1(I2) = C in call I1(E)]] e s ------------------------------------------ VII. parameter lists (3.8) A. as tuples ------------------------------------------ PARAMETER LISTS (3.8) Traditional syntax: D ::= ... | define I(FL) = U FL ::= I:t | I:t , FL U ::= ... | invoke I(AL) AL ::= A | A , AL A ::= N | E | C | L Claim this is cumbersome to write type rules for. Let's see... ------------------------------------------ B. using the correspondence principle ------------------------------------------ KEYWORD PARAMETERS By the correspondence principle, multiple arguments correspond to Keyword parameter syntax: D ::= ... | define I(F) = U F ::= I:t | F1 , F2 U ::= ... | invoke I( Example: var A: newint; proc P(W:int exp, X: int loc, Y: comm, Z: comm -> comm) = (X := W; call Z(Y)); proc Q = A := 0; in call P(fun W = @A+2, proc Y = call Q, alias X = A, proc Z(C:comm) = call C) ------------------------------------------ Why the use of alias to bind X? ------------------------------------------ TYPING RULES FOR KEYWORD PARAMETERS ------------------------------------------ ------------------------------------------ SEMANTICS FOR KEYWORD PARAMETERS ------------------------------------------ How can we tell if parameters are done lazily or not? Does this make the correspondence principle hold? C. another alternative: product types ------------------------------------------ PRODUCT OR TUPLE TYPES As in ML, Haskell, ... D ::= ... | define I(F) = U F ::= I:t U ::= ... | invoke I(A) A ::= N | E | C | L t ::= ... | () | (TL) TL ::= t | t , TL ------------------------------------------ What would the typing rules be? How is this different than passing records? What's the relation between passing records and keyword parameters? VIII. initial environments ------------------------------------------ BUILT-INS VS. INITIAL ENVIRONMENT We have +, not, etc built-in [[ not E ]] env s = not([[E]] env s) [[ E1 + E2]] env s = plus([[E1]] env s, [[E2]] env s) Alternative ------------------------------------------ Does this allow users to redeclare "not"? Is that good? What does this change about the meaning of a program? IX. summary (3.9) ------------------------------------------ SUMMARY (3.9) "A parameterized abstraction is just Hence, lambda abstractions, \I:t . U Language satisfies parameterization principle if: ------------------------------------------ ------------------------------------------ DESIGN METHOD Start with core: - add abstraction forms - add parameter forms Correspondence: makes sure treatment of identifiers that name abstractions and parameters is the same At each step give: - syntax - type attributes - typing rules - denotational semantics - soundness proof ------------------------------------------ Are abstraction and parameterization independent (orthogonal) extensions to the core?