Programming in Standard ML

1 Programming in Standard ML(DRAFT: )Robert HarperCarnegie Mellon UniversitySpring Semester, 2011 Copyrightc 2011 by Robert Rights work is licensed under the Creative CommonsAttribution-Noncommercial-No Derivative Works United StatesLicense. To view a copy of this license, , or send aletter to Creative Commons, 171 Second Street, Suite 300, San Francisco,California, 94105, book is an introduction to Programming with the Standard ML pro-gramming language. It began life as a set of lecture notes for ComputerScience 15 212: Principles of Programming , the second semester of the in-troductory sequence in the undergraduate computer science curriculum atCarnegie Mellon University. It has subsequently been used in many othercourses at Carnegie Mellon, and at a number of universities around theworld. It is intended to supersede myIntroduction to Standard ML, whichhas been widely circulated over the last ten ML is a formally defined Programming Defi-nition of Standard ML (Revised)is the formal definition of the language.

2 Itis supplemented by theStandard ML Basis Library, which defines a com-mon basis of types that are shared by all implementations of the on Standard MLdiscusses some of the decisions that went intothe design of the first version of the are several implementations of Standard ML available for a widevariety of hardware and software platforms. The best-known compilersareStandard ML of New Jersey,MLton,Moscow ML,MLKit, are all freely available on the worldwide web. Please refer toTheStandard ML Home Pagefor up-to-date information on Standard ML andits people have contributed directly and indirectly to this am especially grateful to the following people for their helpful com-ments and suggestions: Brian Adkins, Nels Beckman, Marc Bezem, JamesBostock, Terrence Brannon, Franck van Breugel, Chris Capel, MatthewWilliam Cox, Karl Crary, Yaakov Eisenberg, Matt Elder, Mike Erdmann,Matthias Felleisen, Andrei Formiga, Stephen Harris, Nils J ahnig, Joel Jones,David Koppstein, John Lafferty, Johannes Laire, Flavio Lerda, Daniel , Adrian Moos, Bryce Nichols, Michael Norrish, Arthur J.

3 O Dwyer,Frank Pfenning, Chris Stone, Dave Swasey, Michael Velten, Johan Wallen,Scott Williams, and Jeannette Wing. Richard C. Cobbe helped with font se-lection. I am also grateful to the many students of 15-212 who used thesenotes and sent in their suggestions over the notes are a work in progress. Corrections, comments and sug-gestions are most Overview11 Programming in Standard Regular Expression Package .. Code .. 12II The Core Language132 types , Values, and and Execution .. ML Computation Model .. Checking .. , types , types .. Errors .. Code .. 233 .. Bindings .. Bindings .. Bindings .. Declarations .. Scope .. and Evaluation .. Code .. 324 as Templates .. and Application .. and Scope, Revisited .. Code .. 395 Products and types .. Patterns .. types .. Arguments and Multiple Results.

4 Code .. 506 Case and Heterogeneous types .. Function Expressions .. and Conditionals, Revisited .. and Redundancy .. Code .. 567 Recursive and Recursion .. Reasoning .. Recursion .. Code .. 668 Type Inference and Inference .. Definitions .. Code .. Programming with Primitives .. With Lists .. Code .. 8110 Concrete Data Datatype Declarations .. Non-Recursive Datatypes .. Recursive Datatypes .. Heterogeneous Data Structures .. Abstract Syntax .. Sample Code .. 9111 Higher-Order Functions as Values .. Binding and Scope .. Returning Functions .. Patterns of Control .. Staging .. Sample Code .. 10212 Exceptions as Errors .. Primitive Exceptions .. User-Defined Exceptions .. Exception Handlers .. Value-Carrying Exceptions.

5 Sample Code .. 11213 Mutable Reference Cells .. Reference Patterns .. Identity .. Aliasing .. Programming Well With References .. Private Storage .. Mutable Data Structures .. Mutable Arrays .. Sample Code .. 12614 Textual Input/Output .. Sample Code .. 12915 Lazy Data Lazy Data types .. Lazy Function Definitions .. Programming with Streams .. Sample Code .. 13716 Equality and Equality Sample Code .. 13817 Sample Code .. 139 III The Module Language14018 Signatures and Signatures .. Basic Signatures .. Signature Inheritance .. Structures .. Basic Structures .. Long and Short Identifiers .. Sample Code .. 15019 Signature Principal Signatures .. Matching .. Satisfaction .. Sample Code .. 15720 Signature Ascribed Structure Bindings .. Opaque Ascription .. Transparent Ascription.

6 Sample Code .. 16421 Module Substructures .. Sample Code .. 17322 Sharing Combining Abstractions .. Sample Code .. 18123 Functor Bindings and Applications .. Functors and Sharing Specifications .. Avoiding Sharing Specifications .. Sample Code .. 191IV Programming Techniques19224 Specifications and Specifications .. Correctness Proofs .. Enforcement and Compliance .. 19925 Induction and Exponentiation .. The GCD Algorithm .. Sample Code .. 21126 Structural Natural Numbers .. Lists .. Trees .. Generalizations and Limitations .. Abstracting Induction .. Sample Code .. Proof-Directed Regular Expressions and Languages .. Specifying the Matcher .. Sample Code .. 22828 Persistent and Ephemeral Data Persistent Queues .. Amortized Analysis .. Sample Code .. 23829 Options, Exceptions, and Then-Queens Problem.

7 Solution Using Options .. Solution Using Exceptions .. Solution Using Continuations .. Sample Code .. 24630 Higher-Order Infinite Sequences .. Circuit Simulation .. Regular Expression Matching, Revisited .. Sample Code .. 25631 Cacheing Results .. Laziness .. Lazy Data types in SML/NJ .. Recursive Suspensions .. Sample Code .. 26432 Data Dictionaries .. Binary Search Trees .. Balanced Binary Search Trees .. Checking .. Sample Code .. 27333 Representation Independence and ADT Sample Code .. Modularity and Sample Code .. 27535 Dynamic Typing and Dynamic Sample Code .. 27636 Sample Code .. 277V Appendices278A The Standard ML Basis Library279B Compilation Overview of CM .. Building Systems with CM .. Sample Code .. 281C Sample IOverview2 Standard ML is a type-safe Programming language that embodies manyinnovative ideas in Programming language design.

8 It is a statically typedlanguage, with an extensible type system. It supports polymorphic typeinference, which all but eliminates the burden of specifying types of vari-ables and greatly facilitates code re-use. It provides efficient automaticstorage management for data structures and functions. It encourages func-tional (effect-free) Programming where appropriate, but allows impera-tive (effect-ful) Programming where necessary. It facilitates programmingwith recursive and symbolic data structures by supporting the definitionof functions by pattern matching. It features an extensible exception mech-anism for handling error conditions and effecting non-local transfers ofcontrol. It provides a richly expressive and flexible module system forstructuring large programs, including mechanisms for enforcing abstrac-tion, imposing hierarchical structure, and building generic modules. It isportable across platforms and implementations because it has a precisedefinition.

9 It provides a portable Standard basis library that defines a richcollection of commonly-used types and implementations go beyond the Standard to provide experimen-tal language features, extensive libraries of commonly-used routines, anduseful program development tools. Details can be found with the doc-umentation for your compiler, but here s some of what you may implementations provide an interactive system supporting on-lineprogram development, including tools for compiling, linking, and analyz-ing the behavior of programs. A few implementations are batch compil-ers that rely on the ambient operating system to manage the constructionof large programs from compiled parts. Nearly every compiler generatesnative machine code, even when used interactively, but some also gen-erate code for a portable abstract machine. Most implementations sup-port separate compilation and provide tools for managing large systemsand shared libraries. Some implementations provide tools for tracing andstepping programs; many provide tools for time and space profiling.

10 Mostimplementations supplement the Standard basis library with a rich collec-tion of handy components such as dictionaries, hash tables, or interfaces tothe ambient operating system. Some implementations support languageextensions such as support for concurrent Programming (using message-passing or locking), richer forms of modularity constructs, and support for lazy data 1 Programming in Standard A Regular Expression PackageTo develop a feel for the language and how it is used, let us consider theimplementation of a package for matching strings against regular expres-sions. We ll structure the implementation into two modules, an imple-mentation of regular expressions themselves and an implementation of amatching algorithm for two modules are concisely described by the REGEXP = sigdatatype regexp =Zero | One | Char of char |Plus of regexp * regexp |Times of regexp * regexp |Star of regexpexception SyntaxError of stringval parse : string -> regexpval format : regexp -> stringendsignature MATCHER = sigstructure RegExp : REGEXPval accepts : -> string -> boolendThe signatureREGEXP describes a module that implements regular expres-sions.