The Module System
A theory of dictionaries
In order to illustrate Coq's module system, we
present a theory of dictionnaries implemented as functors,
which is a certified version of an example by L. Paulson in
Standard ML (In ML for the working Programmer, Cambridge University
Press, 1996, pp 280-284)
The complete source
Exercises
-
Improve the module dict by using Standard Library's
RelationClasses for describing abstract properties of relations.
- Write a version of dict using type classes as most as possible.
-
Exercise 12.1 page 339 Lexicographic ordering on lists (with functors)