cardelli s linker Daniel Jackson MIT Lab for Computer Science 6898 Advanced Topics in Software Design March 11 2002 cardelli s motivation separate compilation vital for writing delivering maintaining libraries but often things go wrong module designers lost sight of original aims linking has become complicated so develop a formal model to help reason treat linking outside the programming language Luca Cardelli Program Fragments Linking Modularization POPL 1997 2 separate compilation goofs missing language features no interface impl distinction esp in untyped languages global analysis required multimethods overloading ML modules can t compile library without client templates in C Ada Modula 3 overloading in Java David Griswold runtime type errors despite static types covariance in Eiffel may link with old library by mistake class loading problems 3 our motivation Units a new modularity mechanism will be presented on wednesday by Findler have much in common with Cardelli s model nice example of simple theory shows how to capture essence of a problem use as reference model for more complex systems challenge a nice final project recast Cardelli s theory in Alloy might be simpler no decl ordering check theorems automatically explore variants 4 key ideas focus on type checking the hardest part work at source code level compilation is fragmenting bindings linking is substitution ie inlining linksets a simple configuration language a linkset is a collection of fragments to be linked each fragment has a name a list of imports an export a linkset has an external interface its imports and exports empty for a program non empty for a library 5 judgments the judgment E a A means in the environment E expression a has type A examples f int int f 3 int f int int i int f i int g int int f x return g x int int environment x1 A1 xn An well formed if xi xj for i j 6 lambda calculus variable abstraction application base type function type lambda calculus a toy language for theoretical investigation if you understand Scheme you ll understand it Cardelli uses the variant F1 explicit first order types syntax types A B K A B terms a b x lambda x A b b a 7 type checking expressed as inference rules if f has the type A B in environment E and a has the type A then f a has the type B E f A B E a A E f a B E x A b B E a A E lambda x A b A B E E x E x 8 linksets f lambda x int x int int main f int int f 3 int represents these two fragments fragment f int int import nothing begin lambda x int x end fragment main int import f int int begin f 3 end 9 definitions general form of a linkset L E0 x1 E1 a1 A1 xn En an An defined notions imported names imp L dom E0 exported names exp L x1 xn imported environments imports L E0 exported environments exports L x1 A1 xn An well formed iff imports L and exports L are environments E0 Ei is an environment dom Ei exp L imp L exp L 10 type checking 1 general form of a linkset L E0 x1 E1 a1 A1 xn En an An linkset is intra checked iff E0 is well formed each fragment is well typed in isolation E0 Ei ai Ai 11 type checking 2 general form of a linkset L E0 x1 E1 a1 A1 xn En an An linkset is inter checked iff it s intra checked if Ei has the form E x A E and x is xj then A is Aj type matching here requires exact match could use subtyping instead 12 linking linking steps let L E0 x a A y x A E J then L E0 x a A y E J x a is a linking step write L L for reflexive transitive closure note linking requires an empty environment so build bottom up and no cycles algorithm keep doing linking steps until either linked all environments except E0 empty or stuck no further steps possible and some Ei not empty 13 properties of linking termination compatibility if L and L are compatible linksets and L L then L and L are compatible reduction soundness completeness essentially that algorithm implements maximally linking soundness if inter checked L and L L then inter checked L 14 modules key idea a simple fragment exports a value a module exports a binding client doesn t name the module itself bindings signatures a binding is a list of definitions x int 3 a signature is a list of declarations x int compilation a binding is like a linkset compilation transforms a binding into a linkset 15 separate compilation key theorem given two modules whose interfaces are compatible their compiled linksets are inter checked 16 key ideas two phases intra checking module is well typed inter checking module interfaces match linking criteria easy to understand and predict behaviour allow partial linking order independent linking preserves well formedness properties theory assumes modules are outermost no hiding no mutual references import export types match exactly 17