Ml for the Working Programmer

by Larry C. Paulson

• ISBN13: 9780521570503
• ISBN10: 0521570506
• Edition: 2nd
• Format: Hardcover
• Copyright: 1996-06-28
• Publisher: CAMBRIDGE UNIVERSITY PRESS

Summary

The new edition of this successful and established textbook retains its two original intentions of explaining how to program in the ML language, and teaching the fundamentals of functional programming. The major change is the early and prominent coverage of modules, which the author extensively uses throughout. In addition, Paulson has totally rewritten the first chapter to make the book more accessible to students who have no experience of programming languages. The author describes the main features of new Standard Library for the revised version of ML, and gives many new examples, e.g. polynomial arithmetic and new ways of treating priority queues. Finally he has completely updated the references. Dr. Paulson has extensive practical experience of ML, and has stressed its use as a tool for software engineering; the book contains many useful pieces of code, which are freely available (via Internet) from the author. He shows how to use lists, trees, higher-order functions and infinite data structures. He includes many illustrative and practical examples, covering sorting, matrix operations, and polynomial arithmetic. He describes efficient functional implementations of arrays, queues, and priority queues. Larger examples include a general top-down parser, a lambda-calculus reducer and a theorem prover. A chapter is devoted to formal reasoning about functional programs. The combination of careful explanation and practical advice will ensure that this textbook continues to be the preferred text for many courses on ML for students at all levels.

Table of Contents

Preface to the Second Edition	xiii	(2)
Preface	xv
1 Standard ML	1	(16)
Functional Programming	2	(9)
1.1 Expressions versus commands	2	(1)
1.2 Expressions in procedural programming languages	3	(2)
1.3 Storage management	5	(1)
1.4 Elements of a functional language	5	(4)
1.5 The efficiency of functional programming	9	(2)
Standard ML	11	(6)
1.6 The evolution of Standard ML	11	(1)
1.7 The ML tradition of theorem proving	12	(1)
1.8 The new standard library	13	(2)
1.9 ML and the working programmer	15	(2)
2 Names, Functions and Types	17	(52)
Chapter outline	18	(1)
Value declarations	18	(4)
2.1 Naming constants	18	(1)
2.2 Declaring functions	19	(2)
2.3 Identifiers in Standard ML	21	(1)
Numbers, character strings and truth values	22	(5)
2.4 Arithmetic	22	(2)
2.5 Strings and characters	24	(2)
2.6 Truth values and conditional expressions	26	(1)
Pairs, tuples and records	27	(11)
2.7 Vectors: an example of pairing	28	(1)
2.8 Functions with multiple arguments and results	29	(3)
2.9 Records	32	(4)
2.10 Infix operators	36	(2)
The evaluation of expressions	38	(10)
2.11 Evaluation in ML: call-by-value	39	(1)
2.12 Recursive functions under call-by-value	40	(4)
2.13 Call-by-need, or lazy evaluation	44	(4)
Writing recursive functions	48	(5)
2.14 Raising to an integer power	48	(1)
2.15 Fibonacci numbers	49	(3)
2.16 Integer square roots	52	(1)
Local declarations	53	(6)
2.17 Example: real square roots	54	(1)
2.18 Hiding declarations using local	55	(1)
2.19 Simultaneous declarations	56	(3)
Introduction to modules	59	(4)
2.20 The complex numbers	59	(1)
2.21 Structures	60	(2)
2.22 Signatures	62	(1)
Polymorphic type checking	63	(4)
2.23 Type inference	64	(1)
2.24 Polymorphic function declarations	65	(2)
Summary of main points	67	(2)
3 Lists	69	(54)
Chapter outline	69	(1)
Introduction to lists	70	(4)
3.1 Building a list	70	(2)
3.2 Operating on a list	72	(2)
Some fundamental list functions	74	(8)
3.3 Testing lists and taking them apart	74	(2)
3.4 List processing by numbers	76	(2)
3.5 Append and reverse	78	(3)
3.6 Lists of lists, lists of pairs	81	(1)
Applications of lists	82	(14)
3.7 Making change	83	(2)
3.8 Binary arithmetic	85	(2)
3.9 Matrix transpose	87	(2)
3.10 Matrix multiplication	89	(1)
3.11 Gaussian elimination	90	(3)
3.12 Writing a number as the sum of two squares	93	(2)
3.13 The problem of the next permutation	95	(1)
The equality test in polymorphic functions	96	(12)
3.14 Equality types	97	(1)
3.15 Polymorphic set operations	98	(3)
3.16 Association lists	101	(1)
3.17 Graph algorithms	102	(6)
Sorting: A case study	108	(6)
3.18 Random numbers	108	(1)
3.19 Insertion sort	109	(1)
3.20 Quick sort	110	(1)
3.21 Merge sort	111	(3)
Polynomial arithmetic	114	(7)
3.22 Representing abstract data	115	(1)
3.23 Representing polynomials	116	(1)
3.24 Polynomial addition and multiplication	117	(2)
3.25 The greatest common divisor	119	(2)
Summary of main points	121	(2)
4 Trees and Concrete Data	123	(48)
Chapter outline	123	(1)
The datatype declaration	124	(10)
4.1 The King and his subjects	124	(3)
4.2 Enumeration types	127	(1)
4.3 Polymorphic datatypes	128	(2)
4.4 Pattern-matching with val, as, case	130	(4)
Exceptions	134	(7)
4.5 Introduction to exceptions	134	(1)
4.6 Declaring exceptions	135	(1)
4.7 Raising exceptions	136	(2)
4.8 Handling exceptions	138	(2)
4.9 Objections to exceptions	140	(1)
Trees	141	(7)
4.10 A type for binary trees	142	(3)
4.11 Enumerating the contents of a tree	145	(1)
4.12 Building a tree from a list	146	(2)
4.13 A structure for binary trees	148	(1)
Tree-based data structures	148	(16)
4.14 Dictionaries	149	(5)
4.15 Functional and flexible arrays	154	(5)
4.16 Priority queues	159	(5)
A tautology checker	164	(6)
4.17 Propositional Logic	164	(2)
4.18 Negation normal form	166	(1)
4.19 Conjunctive normal form	167	(3)
Summary of main points	170	(1)
5 Functions and Infinite Data	171	(42)
Chapter outline	171	(1)
Functions as values	172	(7)
5.1 Anonymous functions with fn notation	172	(1)
5.2 Curried functions	173	(3)
5.3 Functions in data structures	176	(1)
5.4 Functions as arguments and results	177	(2)
General-purpose functionals	179	(12)
5.5 Sections	179	(1)
5.6 Combinators	180	(2)
5.7 The list functionals map and filter	182	(2)
5.8 The list functionals takewhile and dropwhile	184	(1)
5.9 The list functionals exists and all	184	(1)
5.10 The list functionals foldl and foldr	185	(3)
5.11 More examples of recursive functionals	188	(3)
Sequences, or infinite lists	191	(13)
5.12 A type of sequences	192	(2)
5.13 Elementary sequence processing	194	(3)
5.14 Elementary applications of sequences	197	(2)
5.15 Numerical computing	199	(2)
5.16 Interleaving and sequences of sequences	201	(3)
Search strategies and infinite lists	204	(7)
5.17 Search strategies in ML	204	(3)
5.18 Generating palindromes	207	(1)
5.19 The Eight Queens problem	208	(2)
5.20 Iterative deepening	210	(1)
Summary of main points	211	(2)
6 Reasoning About Functional Programs	213	(44)
Chapter outline	213	(1)
Some principles of mathematical proof	214	(10)
6.1 ML programs and mathematics	214	(2)
6.2 Mathematical induction and complete induction	216	(4)
6.3 Simple examples of program verification	220	(4)
Structural induction	224	(13)
6.4 Structural induction on lists	225	(4)
6.5 Structural induction on trees	229	(4)
6.6 Function values and functionals	233	(4)
A general induction principle	237	(11)
6.7 Computing normal forms	238	(4)
6.8 Well-founded induction and recursion	242	(4)
6.9 Recursive program schemes	246	(2)
Specification and verification	248	(8)
6.10 An ordering predicate	249	(2)
6.11 Expressing rearrangement through multisets	251	(3)
6.12 The significance of verification	254	(2)
Summary of main points	256	(1)
7 Abstract Types and Functors	257	(56)
Chapter outline	258	(1)
Three representations of queues	258	(5)
7.1 Representing queues as lists	259	(1)
7.2 Representing queues as a new datatype	260	(1)
7.3 Representing queues as pairs of lists	261	(2)
Signatures and abstraction	263	(8)
7.4 The intended signature for queues	263	(1)
7.5 Signature constraints	264	(2)
7.6 The abstype declaration	266	(3)
7.7 Inferred signatures for structures	269	(2)
Functors	271	(14)
7.8 Testing the queue structures	272	(3)
7.9 Generic matrix arithmetic	275	(5)
7.10 Generic dictionaries and priority queues	280	(5)
Building large systems using modules	285	(23)
7.11 Functors with multiple arguments	285	(5)
7.12 Sharing constraints	290	(4)
7.13 Fully-functorial programming	294	(5)
7.14 The open declaration	299	(6)
7.15 Signatures and substructures	305	(3)
Reference guide to modules	308	(4)
7.16 The syntax of signatures and structures	309	(2)
7.17 The syntax of module declarations	311	(1)
Summary of main points	312	(1)
8 Imperative Programming in ML	313	(44)
Chapter outline	313	(1)
Reference types	314	(12)
8.1 References and their operations	314	(3)
8.2 Control structures	317	(4)
8.3 Polymorphic references	321	(5)
References in data structures	326	(14)
8.4 Sequences, or lazy lists	327	(4)
8.5 Ring buffers	331	(4)
8.6 Mutable and functional arrays	335	(5)
Input and output	340	(16)
8.7 String processing	340	(4)
8.8 Text input/output	344	(2)
8.9 Text processing examples	346	(5)
8.10 A pretty printer	351	(5)
Summary of main points	356	(1)
9 Writing Interpreters for the XXX-Calculus	357	(40)
Chapter outline	357	(1)
A functional parser	357	(15)
9.1 Scanning, or lexical analysis	358	(2)
9.2 A toolkit for top-down parsing	360	(3)
9.3 The ML code of the parser	363	(4)
9.4 Example: parsing and displaying types	367	(5)
Introducing the XXX-calculus	372	(6)
9.5 XXX-terms and XXX-reductions	372	(3)
9.6 Preventing variable capture in substitution	375	(3)
Representing XXX-terms in ML	378	(6)
9.7 The fundamental operations	378	(3)
9.8 Parsing XXX-terms	381	(1)
9.9 Displaying XXX-terms	382	(2)
The XXX-calculus as a programming language	384	(12)
9.10 Data structures in the XXX-calculus	385	(3)
9.11 Recursive definitions in the XXX-calculus	388	(1)
9.12 The evaluation of XXX-terms	389	(4)
9.13 Demonstrating the evaluators	393	(3)
Summary of main points	396	(1)
10 A Tactical Theorem Prover	397	(48)
Chapter outline	397	(1)
A sequent calculus for first-order logic	398	(9)
10.1 The sequent calculus for propositional logic	399	(1)
10.2 Proving theorems in the sequent calculus	400	(3)
10.3 Sequent rules for the quantifiers	403	(1)
10.4 Theorem proving with quantifiers	404	(3)
Processing terms and formulae in ML	407	(13)
10.5 Representing terms and formulae	407	(4)
10.6 Parsing and displaying formulae	411	(5)
10.7 Unification	416	(4)
Tactics and the proof state	420	(10)
10.8 The proof state	420	(1)
10.9 The ML signature	421	(3)
10.10 Tactics for basic sequents	424	(2)
10.11 The propositional tactics	426	(2)
10.12 The quantifier tactics	428	(2)
Searching for proofs	430	(14)
10.13 Commands for transforming proof states	430	(3)
10.14 Two sample proofs using tactics	433	(3)
10.15 Tacticals	436	(4)
10.16 Automatic tactics for first-order logic	440	(4)
Summary of main points	444	(1)
Project Suggestions	445	(4)
Bibliography	449	(8)
Syntax Charts	457	(12)
Index	469