You are previewing ML for the Working Programmer, Second Edition.
O'Reilly logo
ML for the Working Programmer, Second Edition

Book Description

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 are extensively used throughout. In addition, the first chapter has been totally rewritten to make the book more accessible to those without experience of programming languages. The main features of new Standard Library for the revised version of ML are described and many new examples are given, while references have also been updated. 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 the Internet) from the author. He shows how to use lists, trees, higher-order functions and infinite data structures. Many illustrative and practical examples are included.. Efficient functional implementations of arrays, queues, priority queues, etc. are described. Larger examples include a general top-down parser, a lambda-calculus reducer and a theorem prover. The combination of careful explanation and practical advice will ensure that this textbook continues to be the preferred text for many courses on ML.

Table of Contents

  1. Cover
  2. Title Page
  3. Copyright Page
  4. Contents
  5. Preface to the Second Edition
  6. Preface
  7. 1 Standard ML
    1. Functional Programming
    2. 1.1 Expressions versus commands
    3. 1.2 Expressions in procedural programming languages
    4. 1.3 Storage management
    5. 1.4 Elements of a functional language
    6. 1.5 The efficiency of functional programming
    7. Standard ML
    8. 1.6 The evolution of Standard ML
    9. 1.7 The ML tradition of theorem proving
    10. 1.8 The new standard library
    11. 1.9 ML and the working programmer
  8. 2 Names, Functions and Types
    1. Chapter outline
    2. Value declarations
    3. 2.1 Naming constants
    4. 2.2 Declaring functions
    5. 2.3 Identifiers in Standard ML
    6. Numbers, character strings and truth values
    7. 2.4 Arithmetic
    8. 2.5 Strings and characters
    9. 2.6 Truth values and conditional expressions
    10. Pairs, tuples and records
    11. 2.7 Vectors: an example of pairing
    12. 2.8 Functions with multiple arguments and results
    13. 2.9 Records
    14. 2.10 Infix operators
    15. The evaluation of expressions
    16. 2.11 Evaluation in ML: call-by-value
    17. 2.12 Recursive functions under call-by-value
    18. 2.13 Call-by-need, or lazy evaluation
    19. Writing recursive functions
    20. 2.14 Raising to an integer power
    21. 2.15 Fibonacci numbers
    22. 2.16 Integer square roots
    23. Local declarations
    24. 2.17 Example: real square roots
    25. 2.18 Hiding declarations using local
    26. 2.19 Simultaneous declarations
    27. Introduction to modules
    28. 2.20 The complex numbers
    29. 2.21 Structures
    30. 2.22 Signatures
    31. Polymorphic type checking
    32. 2.23 Type inference
    33. 2.24 Polymorphic function declarations
    34. Summary of main points
  9. 3 Lists
    1. Chapter outline
    2. Introduction to lists
    3. 3.1 Building a list
    4. 3.2 Operating on a list
    5. Some fundamental list functions
    6. 3.3 Testing lists and taking them apart
    7. 3.4 List processing by numbers
    8. 3.5 Append and reverse
    9. 3.6 Lists of lists, lists of pairs
    10. Applications of lists
    11. 3.7 Making change
    12. 3.8 Binary arithmetic
    13. 3.9 Matrix transpose
    14. 3.10 Matrix multiplication
    15. 3.11 Gaussian elimination
    16. 3.12 Writing a number as the sum of two squares
    17. 3.13 The problem of the next permutation
    18. The equality test in polymorphic functions
    19. 3.14 Equality types
    20. 3.15 Polymorphic set operations
    21. 3.16 Association lists
    22. 3.17 Graph algorithms
    23. Sorting: A case study
    24. 3.18 Random numbers
    25. 3.19 Insertion sort
    26. 3.20 Quick sort
    27. 3.21 Merge sort
    28. Polynomial arithmetic
    29. 3.22 Representing abstract data
    30. 3.23 Representing polynomials
    31. 3.24 Polynomial addition and multiplication
    32. 3.25 The greatest common divisor
    33. Summary of main points
  10. 4 Trees and Concrete Data
    1. Chapter outline
    2. The datatype declaration
    3. 4.1 The King and his subjects
    4. 4.2 Enumeration types
    5. 4.3 Polymorphic datatypes
    6. 4.4 Pattern-matching with val, as, case
    7. Exceptions
    8. 4.5 Introduction to exceptions
    9. 4.6 Declaring exceptions
    10. 4.7 Raising exceptions
    11. 4.8 Handling exceptions
    12. 4.9 Objections to exceptions
    13. Trees
    14. 4.10 A type for binary trees
    15. 4.11 Enumerating the contents of a tree
    16. 4.12 Building a tree from a list
    17. 4.13 A structure for binary trees
    18. Tree-based data structures
    19. 4.14 Dictionaries
    20. 4.15 Functional and flexible arrays
    21. 4.16 Priority queues
    22. A tautology checker
    23. 4.17 Propositional Logic
    24. 4.18 Negation normal form
    25. 4.19 Conjunctive normal form
    26. Summary of main points
  11. 5 Functions and Infinite Data
    1. Chapter outline
    2. Functions as values
    3. 5.1 Anonymous functions with fn notation
    4. 5.2 Curried functions
    5. 5.3 Functions in data structures
    6. 5.4 Functions as arguments and results
    7. General-purpose functionals
    8. 5.5 Sections
    9. 5.6 Combinators
    10. 5.7 The list functionals map and filter
    11. 5.8 The list functionals takewhile and dropwhile
    12. 5.9 The list functionals exists and all
    13. 5.10 The list functionals foldl and foldr
    14. 5.11 More examples of recursive functionals
    15. Sequences, or infinite lists
    16. 5.12 A type of sequences
    17. 5.13 Elementary sequence processing
    18. 5.14 Elementary applications of sequences
    19. 5.15 Numerical computing
    20. 5.16 Interleaving and sequences of sequences
    21. Search strategies and infinite lists
    22. 5.17 Search strategies in ML
    23. 5.18 Generating palindromes
    24. 5.19 The Eight Queens problem
    25. 5.20 Iterative deepening
    26. Summary of main points
  12. 6 Reasoning About Functional Programs
    1. Chapter outline
    2. Some principles of mathematical proof
    3. 6.1 ML programs and mathematics
    4. 6.2 Mathematical induction and complete induction
    5. 6.3 Simple examples of program verification
    6. Structural induction
    7. 6.4 Structural induction on lists
    8. 6.5 Structural induction on trees
    9. 6.6 Function values and functionals
    10. A general induction principle
    11. 6.7 Computing normal forms
    12. 6.8 Well-founded induction and recursion
    13. 6.9 Recursive program schemes
    14. Specification and verification
    15. 6.10 An ordering predicate
    16. 6.11 Expressing rearrangement through multisets
    17. 6.12 The significance of verification
    18. Summary of main points
  13. 7 Abstract Types and Functors
    1. Chapter outline
    2. Three representations of queues
    3. 7.1 Representing queues as lists
    4. 7.2 Representing queues as a new datatype
    5. 7.3 Representing queues as pairs of lists
    6. Signatures and abstraction
    7. 7.4 The intended signature for queues
    8. 7.5 Signature constraints
    9. 7.6 The abstype declaration
    10. 7.7 Inferred signatures for structures
    11. Functors
    12. 7.8 Testing the queue structures
    13. 7.9 Generic matrix arithmetic
    14. 7.10 Generic dictionaries and priority queues
    15. Building large systems using modules
    16. 7.11 Functors with multiple arguments
    17. 7.12 Sharing constraints
    18. 7.13 Fully-functorial programming
    19. 7.14 The open declaration
    20. 7.15 Signatures and substructures
    21. Reference guide to modules
    22. 7.16 The syntax of signatures and structures
    23. 7.17 The syntax of module declarations
    24. Summary of main points
  14. 8 Imperative Programming in ML
    1. Chapter outline
    2. Reference types
    3. 8.1 References and their operations
    4. 8.2 Control structures
    5. 8.3 Polymorphic references
    6. References in data structures
    7. 8.4 Sequences, or lazy lists
    8. 8.5 Ring buffers
    9. 8.6 Mutable and functional arrays
    10. Input and output
    11. 8.7 String processing
    12. 8.8 Text input/output
    13. 8.9 Text processing examples
    14. 8.10 A pretty printer
    15. Summary of main points
  15. 9 Writing Interpreters for the λ-Calculus
    1. Chapter outline
    2. A functional parser
    3. 9.1 Scanning, or lexical analysis
    4. 9.2 A toolkit for top-down parsing
    5. 9.3 The ML code of the parser
    6. 9.4 Example: parsing and displaying types
    7. Introducing the λ-calculus
    8. 9.5 λ-terms and λ-reductions
    9. 9.6 Preventing variable capture in substitution
    10. Representing λ-terms in ML
    11. 9.7 The fundamental operations
    12. 9.8 Parsing λ-terms
    13. 9.9 Displaying λ-terms
    14. The λ-calculus as a programming language
    15. 9.10 Data structures in the λ-calculus
    16. 9.11 Recursive definitions in the λ-calculus
    17. 9.12 The evaluation of λ-terms
    18. 9.13 Demonstrating the evaluators
    19. Summary of main points
  16. 10 A Tactical Theorem Prover
    1. Chapter outline
    2. A sequent calculus for first-order logic
    3. 10.1 The sequent calculus for propositional logic
    4. 10.2 Proving theorems in the sequent calculus
    5. 10.3 Sequent rules for the quantifiers
    6. 10.4 Theorem proving with quantifiers
    7. Processing terms and formulæ in ML
    8. 10.5 Representing terms and formulæ
    9. 10.6 Parsing and displaying formulæ
    10. 10.7 Unification
    11. Tactics and the proof state
    12. 10.8 The proof state
    13. 10.9 The ML signature
    14. 10.10 Tactics for basic sequents
    15. 10.11 The propositional tactics
    16. 10.12 The quantifier tactics
    17. Searching for proofs
    18. 10.13 Commands for transforming proof states
    19. 10.14 Two sample proofs using tactics
    20. 10.15 Tacticals
    21. 10.16 Automatic tactics for first-order logic
    22. Summary of main points
  17. Project Suggestions
  18. Bibliography
  19. Syntax Charts
  20. Index
  21. Predeclared Identifiers