368CS 538 Spring 2006©An Overview of Structures inthe Basis LibraryThe Basis Library contains a widevariety of useful structures. Here is anoverview of some of the mostimportant ones.• OptionOperations for the option type.• BoolOperations for the bool type.• CharOperations for the char type.• StringOperations for the string type.• ByteOperations for the byte type.• IntOperations for the int type.369CS 538 Spring 2006©• IntInfOperations for an unbounded precisioninteger type.• RealOperations for the real type.• MathVarious mathematical values andoperations.• ListOperations for the list type.• ListPairOperations on pairs of lists.• VectorA polymorphic type for immutable(unchangeable) sequences.• IntVector, RealVector,BoolVector, CharVectorMonomorphic types for immutablesequences.370CS 538 Spring 2006©• ArrayA polymorphic type for mutable(changeable) sequences.• IntArray, RealArray,BoolArray, CharArrayMonomorphic types for mutablesequences.• Array2A polymorphic 2 dimensional mutabletype.• IntArray2, RealArray2,BoolArray2, CharArray2Monomorphic 2 dimensional mutabletypes.• TextIOCharacter-oriented text IO.• BinIOBinary IO operations.• OS, Unix, Date, Time, TimerOperating systems types and operations.371CS 538 Spring 2006©ML Type InferenceOne of the most novel aspects of ML isthe fact that it infers types for all userdeclarations.How does this type inference mechanismwork?Essentially, the ML compiler creates anunknown type for each declaration theuser makes. It then solves for theseunknowns using known types and a setof type inference rules. That is, for auser-defined identifieri, ML wants todetermineT(i), the type of i.372CS 538 Spring 2006©The type inference rules are:1. The types of all predefined literals,constants and functions are known inadvance. They may be looked-up andused. For example,2 : inttrue : bool[] : 'a list:: : 'a * 'a list -> 'a list2. All occurrences of the same symbol(using scoping rules) have the sametype.3. In the expressionI = J we know T(I) = T(J).373CS 538 Spring 2006©4. In a conditional(if E1 then E2 else E3) we know thatT(E1) = bool,T(E2) = T(E3) = T(conditional)5. In a function call(f x) we know that if T(f) = 'a -> 'b then T(x) = 'a and T(f x) = 'b6. In a function definitionfun f x = expr; if t(x) = 'a and T(expr) = 'b then T(f) = 'a -> 'b7. In a tuple (e1,e2, ..., en)if we know that T(ei) = 'ai1 ≤ i ≤ n then T(e1,e2, ..., en) = 'a1*'a2*...*'an374CS 538 Spring 2006©8. In a record { a=e1,b=e2, ... } if T(ei) = 'ai1 ≤ i ≤ n then the type of the record ={a:'a1, b:'a2, ...}9. In a list [v1,v2, ... vn]if we know that T(vi) = 'ai1 ≤ i ≤ n then we know that'a1='a2=...='an andT([v1,v2, ... vn]) = 'a1 list375CS 538 Spring 2006©To Solve for Types:1. Assign each untyped symbol its owndistinct type variable.2. Use rules (1) to (9) to solve for andsimplify unknown types.3. Verify that each solution “works”(causes no type errors) throughout theprogram.ExamplesConsiderfun fact(n)=if n=1 then 1 else n*fact(n-1);To begin, we’ll assign type variables:T(fact) = 'a -> 'b(fact is a function)T(n) = 'c376CS 538 Spring 2006©Now we begin to solve for the types'a, 'b and 'c must represent.We know (rule 5) that'c = 'a sincen is the argument of fact.We know (rule 3) that'c = T(1) =int sincen=1 is part of the definition.We know (rule 4) thatT(1) = T(ifexpression)='b since the ifexpression is the body offact.Thus, we have‘a = 'b ='c = int, soT(fact) = int -> intT(n) = intThese types are correct for alloccurrences offact and n in thedefinition.377CS 538 Spring 2006©A Polymorphic Function:fun leng(L) = if L = [] then 0 else 1+len(tl L);To begin, we know thatT([]) = 'a list andT(tl) = 'b list -> 'b listWe assign types to leng and L:T(leng) = 'c -> 'dT(L) = 'eSince L is the argument of leng,'e = 'cFrom the expression L=[] we know'e = 'a list378CS 538 Spring 2006©From the fact that 0 is the result ofthe then, we know the if returns anint, so 'd = int.ThusT(leng) = 'a list -> int andT(L) = 'a listThese solutions are type correctthroughout the definition.379CS 538 Spring 2006©Type Inference for PatternsType inference works for patterns too.Considerfun leng [] = 0 | leng (a::b) = 1 + leng b;We first create type variables:T(leng) = 'a -> 'bT(a) = 'cT(b) = 'dFrom leng [] we conclude that'a = 'e listFrom leng [] = 0 we conclude that'b = intFrom leng (a::b) we conclude that'c ='e and 'd = 'e listThus we haveT(leng) = 'e list -> int380CS 538 Spring 2006©T(a) = 'eT(b) = 'e listThis solution is type correctthroughout the definition.381CS 538 Spring 2006©Not Everything can beAutomatically Typed in MLLet’s try to typefun f x = (x x);We assumeT(f) = 'a -> 'bt(x) = 'cNow (as usual) 'a = 'c since x is theargument off.From the call(x x) we conclude that'c must be of the form 'd -> 'e(since x is being used as a function).Moreover,'c = 'd since x is anargument in(x x).Thus'c = 'd ->'e = 'c ->'e.But'c = 'c->'e has no solution, soin ML this definition is invalid. We382CS 538 Spring 2006©can’t pass a function to itself as anargument—the type system doesn’tallow it.In Scheme this is allowed:(define (f x) (x x))but a call like(f f)certainly doesn’t do anything good!383CS 538 Spring 2006©Type UnionsLet’s try to typefun f g = ((g 3), (g true));Now the type of g is 'a -> 'b since gis used as a function.The call(g 3) says 'a = int and thecall(g true) says 'a = boolean.Does this meang is polymorphic?That is, is the type offf : ('a->'b)->'b*'b?NO!All functions have the type'a -> 'bbut not all functions can be passed tof.Considernot: bool->bool.The call(not 3) is certainly illegal.384CS 538 Spring 2006©What we’d like in this case is a uniontype. That is, we’d like to be able totypeg as (int|bool)->'b which MLdoesn’t allow.Fortunately, ML does allow typeconstructors, which are just what weneed.Givendatatype T = I of int|B of bool;we can redefine f asfun f g = (g (I(3)), g (B(true)));valf=fn:(T->'a)->'a*'a385CS 538 Spring 2006©Finally, note that in a definition likelet val f =fn x => x (* id function*)in (f 3,f true)end;type inference works fine:val it = (3,true) : int * boolHere we define f in advance, so itstype is known when calls to it