Type Systems for Programming Languages 1 (DRAFT)

TypeSystemsforProgrammingLanguages1(DRAFT)RobertHarperSchoolofComputerScienceCarnegieMellonUniversityPittsburgh,PA15213-3891E-mail:[e-mail]://~rwhSpring,2000Copyrightc1995-2000.Allrightsreserved.1ThesearecoursenotesComputerScience15–814atCarnegieMellonUniversity.Thisisanincomplete,workingdraft,notintendedforpublication.Citationstotheliteraturearespottyatbest;noresultspresentedhereshouldbeconsideredoriginalunlessexplicitlystatedotherwise.Pleasedonotdistributethesenoteswithoutthepermissionoftheauthor.iiContentsITypeStructure11BasicTypes31.1Introduction..............................31.2Statics.................................31.3Dynamics...............................41.3.1ContextualSemantics....................41.3.2EvaluationSemantics....................51.4TypeSoundness...........................71.5References...............................82FunctionandProductTypes92.1Introduction..............................92.2Statics.................................92.3Dynamics...............................102.4TypeSoundness...........................112.5Termination..............................122.6References...............................133Sums153.1Introduction..............................153.2SumTypes..............................153.3References...............................164Subtyping174.1Introduction..............................174.2Subtyping...............................174.2.1Subsumption.........................184.3PrimitiveSubtyping.........................184.4TupleSubtyping...........................194.5RecordSubtyping...........................224.6References...............................24iii5VariableTypes255.1Introduction..............................255.2VariableTypes............................255.3TypeDefinitions...........................265.4Constructors,Types,andKinds...................285.5References...............................306RecursiveTypes316.1Introduction..............................316.2G¨odel’sT...............................316.2.1Statics.............................316.2.2Dynamics...........................326.2.3Termination..........................326.3Mendler’sS..............................346.4GeneralRecursiveTypes.......................366.5References...............................377Polymorphism397.1Introduction..............................397.2Statics.................................397.3Dynamics...............................407.4ImpredicativePolymorphism....................417.4.1Termination..........................427.4.2DefinabilityofTypes.....................467.5References...............................478AbstractTypes498.1Statics.................................498.2Dynamics...............................508.3Impredicativity............................508.4DotNotation.............................518.5References...............................539HigherKinds559.1Introduction..............................559.2FunctionalKinds...........................559.3SubtypingandHigherKinds....................569.4BoundedQuantificationandPowerKinds.............579.5SingletonKinds,DependentKinds,andSubkinding........599.6References...............................5910Modularity6110.1Introduction..............................6110.2ACritiqueofSomeModularityMechanisms............6810.3AModulesLanguage.........................7110.3.1Structures...........................72iv10.3.2ModuleHierarchies......................7610.3.3ParameterizedModules...................7710.4Second-ClassModules........................7910.5Higher-OrderModules........................7910.6References...............................7911Objects8111.1Introduction..............................8111.2PrimitiveObjects...........................8111.3ObjectSubtyping...........................8111.4Second-OrderObjectTypes.....................8111.5References...............................8112DynamicTypes8312.1TypeDynamic............................8312.2HierarchicalTagging.........................8313Classes8513.1Introduction..............................8513.2Public,Private,andProtected...................8513.3Constructors.............................8513.4SubtypingandInheritance......................8513.5DynamicDispatch..........................8513.6References...............................85IIComputationalEffects8714RecursiveFunctions8914.1Introduction..............................8914.2Statics.................................8914.3Dynamics...............................9014.4TypeSoundness...........................9014.5Compactness.............................9114.6References...............................9315Continuations9515.1Introduction..............................9515.2Statics.................................9515.3Dynamics...............................9615.4Soundness...............................9815.5References...............................100v16References10116.1Introduction..............................10116.2Statics.................................10116.3Dynamics..........