Type SystemsHaskell & ML: Interesting FeaturesType InferencingType Inferencing (cont)PolymorphismPolymorphism (cont)Polymorphism (Cardelli & Wegner)More TermsPolymorphism: A TaxonomyExploring Terminology…Cardelli on Type SystemsMore Cardelli on TypesSafety and Typed LanguagesOff on Good BehaviorSafety and TypedML Type InferencingType Variables/InstancesSubstitution/UnificationMost General UnifiersML Type Inferencing ExampleML Type Inferencing Example (2)Constraint-Based Type Inference and Parametric Polymorphism Ole Agesen (Stanford) 1994Three Step Process: Steps 1 & 2Three Step Process: Step 3Slide 25Slide 26Slide 27Inference Algorithms1-Level Expansion Algorithm: FailureP-Level Expansion AlgorithmAdaptive Inference AlgorithmsSlide 32Slide 33Slide 34Hash Function Algorithm (3)Iterative AlgorithmIterative Algorithm (2)SummaryType SystemsType Systems31 March 1999 CS655 - P.F. ReynoldsHaskell & ML: Interesting FeaturesHaskell & ML: Interesting Features•Type inferencing•Freedom from side effects•Pattern matching•Polymorphism•Support for higher order functions•Lazy patterns / lazy evaluation•Support for object-oriented programming31 March 1999 CS655 - P.F. ReynoldsType InferencingType Inferencing•Def: ability of the language to infer types without having programmer provide type signatures.–SML e.g.:fun min (a: real, b)= if a > bthen belse a–type of a has to be given, but then that’s sufficient to figure out•type of b•type of min–What if type of a is not specified?- could be ints- could be bools...31 March 1999 CS655 - P.F. ReynoldsType Inferencing (cont)Type Inferencing (cont)•Haskell (as with ML) guarantees type safety–Haskell example:eq = (a = b)–a polymorphic function that has a return type of bool,• assumes only that its two arguments are of the same type and can have the equality operator applied to them.–ML has similar assumption, for what it calls equality types.•Overuse of type inferencing in both languages is discouraged–declarations are a design aid–declarations are a documentation aid–declarations are a debugging aid31 March 1999 CS655 - P.F. ReynoldsPolymorphismPolymorphism•ML:fun factorial (0) = 1= | factorial (n) = n * factorial (n - 1)–ML infers factorial is an integer function: int -> int•Haskell:factorial (0) = 1factorial (n) = n * factorial (n - 1)–Haskell infers factorial is a (numerical) function: Num a => a -> a31 March 1999 CS655 - P.F. ReynoldsPolymorphism (cont)Polymorphism (cont)•ML:fun mymax(x,y) = if x > y then x else y–SML infers mymax is ambiguousfun mymax(x: real ,y) = if x > y then x else y–SML infers mymax is real•Haskell:mymax(x,y) = if x > y then x else y–Haskell infers mymax is an Ord function31 March 1999 CS655 - P.F. ReynoldsPolymorphism (Cardelli & Wegner)Polymorphism (Cardelli & Wegner)• Universe, V, of all values• A Type is a set of values selected from V (subset of V)• Sometimes only way to enumerate is through constants and functions• An Ideal is a type that satisfies certain "technical" properties• (one would not identify a type containing integers and Int-> Int functions)• All types found in programming languages are ideals• (Value) Having a type::= membership in a set.• Because ideals can overlap, a value can have many types• A type system (in a language) is a collection of ideals of V• Languages provide support for defining which types are mappable onto ideals31 March 1999 CS655 - P.F. ReynoldsMore TermsMore Terms•Monomorphic Type System: a value belongs to at most one type•Polymorphic Type System: a value may belong to many types•Mostly Monomorphic . . . Mostly Polymorphic–One or the other characterizes individual languages•Polymorphism, as it relates to:–values and variables: may have more than one type–functions: arguments can be of > one type–types: operations are applicable to operands of more than one typePolymorphism: A TaxonomyPolymorphism: A TaxonomyParametric: uniformity of type structure is achieved by type parametersInclusion: object can belong to many different classes that need not be disjoint (subtypes & inheritance)Overloading: same name used to denote different functions. Use determined from contextCoercion: a semantic operation required to convert an argument to a type expected by a function.UniversalAd HocPolymorphismUniversal: infinite number of types with common structureAd Hoc: finite set of potentially unrelated types.31 March 1999 CS655 - P.F. ReynoldsExploring Terminology…Exploring Terminology…•Is inclusion polymorphism a kind of parametric polymorphism?–Consider invocation of a method (behavior) in C++ (Smalltalk): selection is based (parametrically) on type…–Why is inclusion polymorphism not a form of parametric polymorphism?•Are generics (templates) a form of universal polymorphism?–Cardelli & Wegner: no–Day et. al.: yes (parametric)•Is there a difference between/among subtypes, subclasses and inheritance?–Subtypes: derived type’s methods/data subsume parent type’s–Subclasses: structuring–Inheritance: subtypes + subclasses -> specialization31 March 1999 CS655 - P.F. ReynoldsCardelli on Type SystemsCardelli on Type Systems•Type system–purpose is to prevent occurrence of execution errors during runtime•Type Sound Language–absence of execution errors holds for all program runs that can be described in a programming language•Typechecker–method for determining if type errors occur–ambiguities in language specifications often lead to different type checker implementations, hampering language soundness.•Type–“Upper bound” (maximal set) on range of values a variable can take on•Typed Language–one in which variables can be given (nontrivial) typesHow about “can assume”?31 March 1999 CS655 - P.F. ReynoldsMore Cardelli on TypesMore Cardelli on Types•Explicit / implicit typing–as names suggest…•Trapped errors–execution error when computation stops “immediately”•Untrapped errors–execution errors that go unnoticed and cause arbitrary behavior•Safe program fragment–one that does not (cannot?) cause untrapped errors to occur•Safe language–one in which all program fragments are safe31 March 1999 CS655 - P.F. ReynoldsSafety and Typed LanguagesSafety and Typed Languages•“Untyped languages may enforce safety by performing run time checks.”•“Typed languages may also use a