Programming in Standard ML

1 Programming in Standard ML. (D RAFT: V ERSION OF ). Robert Harper Carnegie Mellon University Spring Semester, 2011. Copyright 2011. c by Robert Harper. All Rights Reserved. This work is licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works United States License. To view a copy of this license, visit , or send a letter to Creative Commons, 171 Second Street, Suite 300, San Francisco, California, 94105, USA. Preface This book is an introduction to Programming with the Standard ML pro- gramming language. It began life as a set of lecture notes for Computer Science 15 212: Principles of Programming , the second semester of the in- troductory sequence in the undergraduate computer science curriculum at Carnegie Mellon University. It has subsequently been used in many other courses at Carnegie Mellon, and at a number of universities around the world. It is intended to supersede my Introduction to Standard ML, which has been widely circulated over the last ten years.

2 Standard ML is a formally defined Programming language. The Defi- nition of Standard ML (Revised) is the formal definition of the language. It is supplemented by the Standard ML Basis Library, which defines a com- mon basis of types that are shared by all implementations of the language. Commentary on Standard ML discusses some of the decisions that went into the design of the first version of the language. There are several implementations of Standard ML available for a wide variety of hardware and software platforms. The best-known compilers are Standard ML of New Jersey, MLton, Moscow ML, MLKit, and PolyML. These are all freely available on the worldwide web. Please refer to The Standard ML Home Page for up-to-date information on Standard ML and its implementations. Numerous people have contributed directly and indirectly to this text. I am especially grateful to the following people for their helpful com- ments and suggestions: Brian Adkins, Nels Beckman, Marc Bezem, James Bostock, Terrence Brannon, Franck van Breugel, Chris Capel, Matthew William 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 R.

3 Licata, Adrian Moos, Bryce Nichols, Michael Norrish, Arthur J. 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 these notes and sent in their suggestions over the years. These notes are a work in progress. Corrections, comments and sug- gestions are most welcome. Contents Preface ii I Overview 1. 1 Programming in Standard ML 3. A Regular Expression Package .. 3. Sample Code .. 12. II The Core Language 13. 2 Types, Values, and Effects 15. Evaluation and Execution .. 15. The ML Computation Model .. 16. Type Checking .. 17. Evaluation .. 19. Types, Types, Types .. 21. Type Errors .. 23. Sample Code .. 23. 3 Declarations 24. Variables .. 24. Basic Bindings .. 25. Type Bindings .. 25. Value Bindings .. 26. Compound Declarations .. 27. Limiting Scope .. 28. CONTENTS vi Typing and Evaluation.

4 29. Sample Code .. 32. 4 Functions 33. Functions as Templates .. 33. Functions and Application .. 34. Binding and Scope, Revisited .. 37. Sample Code .. 39. 5 Products and Records 40. Product Types .. 40. Tuples .. 40. Tuple Patterns .. 42. Record Types .. 45. Multiple Arguments and Multiple Results .. 48. Sample Code .. 50. 6 Case Analysis 51. Homogeneous and Heterogeneous Types .. 51. Clausal Function Expressions .. 52. Booleans and Conditionals, Revisited .. 53. Exhaustiveness and Redundancy .. 54. Sample Code .. 56. 7 Recursive Functions 57. Self-Reference and Recursion .. 58. Iteration .. 61. Inductive Reasoning .. 62. Mutual Recursion .. 65. Sample Code .. 66. 8 Type Inference and Polymorphism 67. Type Inference .. 67. Polymorphic Definitions .. 70. Overloading .. 73. Sample Code .. 76. R EVISED D RAFT V ERSION CONTENTS vii 9 Programming with Lists 77. List Primitives .. 77. Computing With Lists .. 79. Sample Code .. 81. 10 Concrete Data Types 82.

5 Datatype Declarations .. 82. Non-Recursive Datatypes .. 83. Recursive Datatypes .. 85. Heterogeneous Data Structures .. 88. Abstract Syntax .. 89. Sample Code .. 91. 11 Higher-Order Functions 92. Functions as Values .. 92. Binding and Scope .. 93. Returning Functions .. 95. Patterns of Control .. 97. Staging .. 99. Sample Code .. 102. 12 Exceptions 103. Exceptions as Errors .. 104. Primitive Exceptions .. 104. User-Defined Exceptions .. 105. Exception Handlers .. 107. Value-Carrying Exceptions .. 110. Sample Code .. 112. 13 Mutable Storage 113. Reference Cells .. 113. Reference Patterns .. 115. Identity .. 116. Aliasing .. 118. Programming Well With References .. 119. Private Storage .. 120. Mutable Data Structures .. 122. Mutable Arrays .. 124. R EVISED D RAFT V ERSION CONTENTS viii Sample Code .. 126. 14 Input/Output 127. Textual Input/Output .. 127. Sample Code .. 129. 15 Lazy Data Structures 130. Lazy Data Types .. 132. Lazy Function Definitions.

6 133. Programming with Streams .. 135. Sample Code .. 137. 16 Equality and Equality Types 138. Sample Code .. 138. 17 Concurrency 139. Sample Code .. 139. III The Module Language 140. 18 Signatures and Structures 142. Signatures .. 142. Basic Signatures .. 143. Signature Inheritance .. 144. Structures .. 147. Basic Structures .. 147. Long and Short Identifiers .. 148. Sample Code .. 150. 19 Signature Matching 151. Principal Signatures .. 152. Matching .. 153. Satisfaction .. 157. Sample Code .. 157. 20 Signature Ascription 158. Ascribed Structure Bindings .. 158. Opaque Ascription .. 159. R EVISED D RAFT V ERSION CONTENTS ix Transparent Ascription .. 162. Sample Code .. 164. 21 Module Hierarchies 165. Substructures .. 165. Sample Code .. 173. 22 Sharing Specifications 174. Combining Abstractions .. 174. Sample Code .. 181. 23 Parameterization 182. Functor Bindings and Applications .. 182. Functors and Sharing Specifications .. 185. Avoiding Sharing Specifications.

7 187. Sample Code .. 191. IV Programming Techniques 192. 24 Specifications and Correctness 194. Specifications .. 194. Correctness Proofs .. 196. Enforcement and Compliance .. 199. 25 Induction and Recursion 202. Exponentiation .. 202. The GCD Algorithm .. 207. Sample Code .. 211. 26 Structural Induction 212. Natural Numbers .. 212. Lists .. 214. Trees .. 215. Generalizations and Limitations .. 216. Abstracting Induction .. 217. Sample Code .. 219. R EVISED D RAFT V ERSION CONTENTS x 27 Proof-Directed Debugging 220. Regular Expressions and Languages .. 220. Specifying the Matcher .. 222. Sample Code .. 228. 28 Persistent and Ephemeral Data Structures 229. Persistent Queues .. 232. Amortized Analysis .. 235. Sample Code .. 238. 29 Options, Exceptions, and Continuations 239. The n-Queens Problem .. 239. Solution Using Options .. 241. Solution Using Exceptions .. 242. Solution Using Continuations .. 244. Sample Code .. 246. 30 Higher-Order Functions 247.

8 Infinite Sequences .. 248. Circuit Simulation .. 251. Regular Expression Matching, Revisited .. 254. Sample Code .. 256. 31 Memoization 257. Cacheing Results .. 257. Laziness .. 259. Lazy Data Types in SML/NJ .. 261. Recursive Suspensions .. 263. Sample Code .. 264. 32 Data Abstraction 265. Dictionaries .. 266. Binary Search Trees .. 266. Balanced Binary Search Trees .. 268. Abstraction vs. Run-Time Checking .. 272. Sample Code .. 273. 33 Representation Independence and ADT Correctness 274. Sample Code .. 274. R EVISED D RAFT V ERSION CONTENTS xi 34 Modularity and Reuse 275. Sample Code .. 275. 35 Dynamic Typing and Dynamic Dispatch 276. Sample Code .. 276. 36 Concurrency 277. Sample Code .. 277. V Appendices 278. A The Standard ML Basis Library 279. B Compilation Management 280. Overview of CM .. 281. Building Systems with CM .. 281. Sample Code .. 281. C Sample Programs 282. R EVISED D RAFT V ERSION Part I. Overview 2. Standard ML is a type-safe Programming language that embodies many innovative ideas in Programming language design.

9 It is a statically typed language, with an extensible type system. It supports polymorphic type inference, which all but eliminates the burden of specifying types of vari- ables and greatly facilitates code re-use. It provides efficient automatic storage 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 Programming with recursive and symbolic data structures by supporting the definition of functions by pattern matching. It features an extensible exception mech- anism for handling error conditions and effecting non-local transfers of control. It provides a richly expressive and flexible module system for structuring large programs, including mechanisms for enforcing abstrac- tion, imposing hierarchical structure, and building generic modules. It is portable across platforms and implementations because it has a precise definition.

10 It provides a portable Standard basis library that defines a rich collection of commonly-used types and routines. Many implementations go beyond the Standard to provide experimen- tal language features, extensive libraries of commonly-used routines, and useful program development tools. Details can be found with the doc- umentation for your compiler, but here's some of what you may expect. Most implementations provide an interactive system supporting on-line program 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 construction of large programs from compiled parts. Nearly every compiler generates native 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 systems and shared libraries.