Types and Programming Languages The Next …

1 Types and Programming LanguagesThe Next GenerationBenjamin C. PierceUniversity of PennsylvaniaLICS, 20031/89 OverviewBirds-eye view of what s happening in the world of typesfor Programming Languages (not logic or theorem proving)Using 1993 and 2003 as reference points2/89 CaveatsI ll painting with a broad brush painting with a lot of people s paints making a quick sketch, not a finished landscapeand giving few citations!3/89 Overview Some changes in the PL world4/89 Overview Some changes in the PL world Some mature research areas4/89 Overview Some changes in the PL world Some mature research areas Some still going strong areas4/89 Overview Some changes in the PL world Some mature research areas Some still going strong areas Some new kids on the block4/89 Overview Some changes in the PL world Some mature research areas Some still going strong areas Some new kids on the block Some current trends and challenges4/89 Some Big Changes5/89We ve come a long way.

2 BabyIt doesn t always feel like it when you are working in thetrenches, but the world of PL research has changed insome major ways in ten Java (and C#) JuggernautThe end of the argument about safe Languages , Types ,garbage collection, etc., Hits the Big TimeA side effect of the success of Java and C# is that proofcarrying code isalreadytaking over as a standard formatfor exchanging and installing code over the net. Java and C# are simple instances (proofs typingderivations or annotations that can be used toreconstruct them) much more ambitious variants are being proposed[foundational PCC, etc.]

3 ]8/89 Technology TransfersIndustrial interest shortening time-horizon for (at leastsome) technology transfer Transferring garbage collection into mainstreamlanguages took 30years Transferring F-bounded quantification and local typeinference into Java (to form GJ) took 5years9/89 The security boomBrought to you by the recent explosion and imminentcollapse of the least some parts of the world ( funding agencies)are waking up to the urgency of better software link with PL:Can t build castles out of cardboard!Less trivial:Maybe we can bring techniques and insightsfrom Programming Languages to bear on understanding,formalizing, and checking real security properties (secrecy, authenticity, anonymity, etc.)

4 , etc.).10/89 Rise of Lightweight Formal Methods Formal methods will never have any impact until theycan be used by people that don t understand them. (attributed to) Tom MelhamDon t prove correctness; just find Model checking Light specification and verification[ESC, SLAM, etc.](not always even sound!) Typechecking!The basic ideas are long-established; but industrialattitudes have been greatly softened by the success ofmodel checking in hardware Type SystemsPeople are getting more courageouscavalier?about working withcomplex type systems Surprisingly complex type systems are being usednow in the real world (cf.

5 GJ!) Verycomplex type systems are being explored inresearchType systems are also gettingricher being used totrack stronger and stronger invariants on data objects andtheir assumptions about their environment12/89 Pervasive Presence of PiAnother result (?)..The pi-calculus[Milner-Parrow-Walker]has had a hugeinfluence on the PL research world. compelling in itself first concurrent calculus to be both powerful enough (to encodelambda-calculus, ) and also mathematically elegant and tractable popularized operational techniques such asbisimulation focused attention on name binding ( )One result.

6 Most PL people today know something a big change from ten years ago13/89 Triumph of Operational SemanticsSince the early 90s, the focus in the PL community hasmoved from denotational descriptions and proof techniquesto operational ones closer to PL practice (abstract machines) lower-level easier to deal with wide range oflanguage features (in particular, concurrency!) increasingly powerful proof techniques becomingavailable[Pitts, etc.]14/89 One Mature Area:6= finished !Object Types15/89 OverviewGoal: Formalize / explain core features of OO languagesby compilation into some typed lambda-calculusThere is some disagreement about what are the corefeatures, but people pretty much agree at least on: OO-style abstraction subtyping subclassing (or method override) open recursion throughself( )16/89 TimelinePrehistory1983A Semantics of Multiple Inheritance[Cardelli]1989 Inheritance is not Subtyping[Cook, Hill, Canning]Results1993A Paradigmatic Object-Oriented Programming language .

7 Design, Static Typing and Semantics[Bruce]1993 Object-Oriented Programming Without Recursive Types [Pierce-Turner]1994A Theory of Objects[Abadi-Cardelli]Refinements1996On Binary Methods[Bruce-Cardelli-Castagna-HOG-Leav ens-Pierce]1996An Interpretation of Objects and Object Types [Abadi-Cardelli-Viswanathan]1997 Comparing Object Encodings[Bruce-Cardelli-Pierce]Explotat ion1996 Objective ML: A simple object-oriented extension of ML[R my-Vouillon]1998 Making the Future Safe for the Past: Adding Genericity to the JavaProgramming language [Bracha-Odersky-Stoutamire-Wadle r]2001 Design and Implementation of Generics for the.

8 NET CommonLanguage Runtime[Kennedy-Syme]17/89OC vs. lambda-calculus encodingsThe object calculus and lambda-calculus approaches arefundamentally very similar they deal with the same range ofphenomena and rely on essentially the same typing , the object calculus has proved more popular. Why? Immediacy: OC is obviouslyobject-oriented appealing Implementability: operational semantics of OC is close to something one could imagineimplementing directly (though few people have!). operational behavior of lambda-calculus encodings is easy to getright modulo efficiency but challenging to work out in a way thatwould satisfy an OO compiler writer Inflexibility: OC (in original form) does not support depthsubtyping ({x:A,y:C} {x:B,y:C}ifA B)Leads to nice simplification of the theorySame restriction possible in -calculi, but feels unnatural 18/89 Technical ChallengeWhat is the precise relation between structural andnominal type systems?

9 Structural:type names are just abbreviations for (completelyinterchangeable with) their definitions; type equivalence,subtyping, etc. follow structureused in most research on type systems nominal:type names matter; subtyping declared byprogrammer (checked for consistency by compiler)used in most mainstream OO Languages (GJ and C# generics are actually a complex hybrid)Is there a general way to transfer mechanisms / resultsfrom one setting to the other?19/89 Technical ChallengeWhat is the precise relation between structural andnominal type systems? structural:type names are just abbreviations for (completelyinterchangeable with) their definitions; type equivalence,subtyping, etc.

10 Follow structureused in most research on type systems nominal:type names matter; subtyping declared byprogrammer (checked for consistency by compiler)used in most mainstream OO Languages (GJ and C# generics are actually a complex hybrid)Is there a general way to transfer mechanisms / resultsfrom one setting to the other?Cardelli-Gosling isomorphism, anyone?19/89 Another ChallengeExplaining polymorphic OO Programming to the masses golden opportunity for a good textbook![your name here]20/89 Some Ongoing Areasand still surprisingly Quantification22/89 Basic IdeaCombine universal a twist:All X Understanding Types , Data Abstraction, and Polymorphism[Cardelli-Wegner]( Kernel F )1990 92 Coherence of Subsumption.