Using Coq to Understand Nested Datatypes

摘要

Nested datatypes can be denned in a Hindley-Milner system but it is difficult to implement functions on them. This paper analyzes the requirements that must be satisfied in order to implement programs (catamorphisms and anamorphisms) on these types. A solution, using Hagino's approach, is carried out here both in Haskell, using rank 2 signatures, and in the Coq proof assistant system where we have polymorphic recursion and also the capability to prove the correspondent programs specifications.