Programming Languages Build, Prove, and Compare

Typed Impcore and Typed ρScheme represent two extremes. Typed Impcore is easy to program in and easy to write a type checker for, but because it is monomorphic, it cannot accept polymorphic functions, and it can accommodate new type constructors and polymorphic operations only if its syntax and type checker are extended. Typed μScheme is also easy to write a type checker for, and as a polymorphic language, it can accept polymorphic functions, and it can accommodate new type constructors and polymorphic functions with no change to its syntax or its type checker. But Typed μScheme is difficult to program in: as Milner observed, supplying a type parameter at every use of every polymorphic value soon becomes intolerable. To combine the expressive power of polymorphism with great ease of programming, this chapter presents a third point in the design space: nano-ML. Nano-ML is expressive, easy to extend, and also easy to program in. This ease of use is delivered by a new typing algorithm: instead of type checking, nano-ML uses type inference.