Type Systems Haskell 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 programming 31 March 1999 CS655 P F Reynolds Type Inferencing Def ability of the language to infer types without having programmer provide type signatures SML e g fun min a real if a b then b else a b 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 Reynolds 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 aid 31 March 1999 CS655 P F Reynolds Polymorphism ML fun factorial 0 1 factorial n n factorial n 1 ML infers factorial is an integer function int int Haskell factorial 0 1 factorial n n factorial n 1 Haskell infers factorial is a numerical function Num a a a 31 March 1999 CS655 P F Reynolds Polymorphism cont ML fun mymax x y if x y then x else y SML infers mymax is ambiguous fun 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 function 31 March 1999 CS655 P F Reynolds 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 ideals 31 March 1999 CS655 P F Reynolds More 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 functions types 31 March 1999 may have more than one type arguments can be of one type operations are applicable to operands of more than one type CS655 P F Reynolds Polymorphism A Taxonomy Universal infinite number of types with common structure Universal Polymorphism Ad Hoc Parametric uniformity of type structure is achieved by type parameters Inclusion 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 context Coercion a semantic operation required to convert an argument to a type expected by a function Ad Hoc finite set of potentially unrelated types 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 specialization 31 March 1999 CS655 P F Reynolds Cardelli 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 types How about can assume 31 March 1999 CS655 P F Reynolds More 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 safe 31 March 1999 CS655 P F Reynolds Safety and Typed Languages Untyped languages may enforce safety by performing run time checks Typed languages may also use a mixture of run time and static checks Is an untyped language that enforces safety comprehensively at run time equivalent to a typed language that uses run time checks exclusively 31 March 1999 CS655 P F Reynolds Off on Good Behavior Forbidden errors all untrapped errors plus some trapped errors what trapped errors might be included Good Behavior well behaved no forbidden errors occur a well behaved program fragment is safe Strongly checked language One in which all legal program fragments have good behavior no untrapped errors occur none of the specified trapped errors occur other trapped errors may occur programmer must avoid them notice avoidance of strongly typed 31 March 1999 CS655 P F Reynolds Safety and Typed Safe Unsafe Typed Untyped ML C LISP Assembler Cardelli argues languages should be safe and typed Should type system be implicit or explicit or both 31 March 1999 CS655 P F Reynolds ML Type Inferencing Key concepts Type variables Substitution Unification Most general unifiers Inferencing Hindley Milner 31 March 1999 CS655 P F Reynolds Type Variables Instances Type variables tyvar identifier e g a b m provide for polymorphism Type instances int a int list a int list a list int a list int is an instance of a list of ints is an instance of a int list is an instance of list of a int is NOT an instance of list of a A precise definition requires substitution for type variables 31 March 1999 CS655 P F Reynolds Substitution Unification Substitution replacement of type variable by another type variable or a concrete type e g Replacing a by int or a by b list Unification t1 and t2 are unified by