Datatypes parameterized over Typerecords
Talk given at the Dagstuhl Seminar Dependent Type Theory meets Practical Programming August 2001.
We discuss a programming exercise in which we have generalized Tim Sheard's generic unification algorithm (ICFP'01) to cope with mutually recursive term datatypes. The programming language of choice is Cayenne, where we use dependent types to encode records of types for the recursive parameter in the term datatypes.
Slides in compressed PostScript.