Transcription of 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.
2 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. 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.
3 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.
4 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.
5 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 .. Code .. 506 Case and Heterogeneous Types.
6 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.
7 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 .. Sample Code .. 11213 Mutable Reference Cells .. Reference Patterns .. Identity .. Aliasing.
8 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.
9 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 .. Sample Code .. 16421 Module Substructures .. Sample Code .. 17322 Sharing Combining Abstractions .. Sample Code .. 18123 Functor Bindings and Applications .. Functors and Sharing Specifications.
10 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.
