Mercurial > cpdt > repo
comparison src/Generic.v @ 465:4320c1a967c2
Spell check
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 29 Aug 2012 18:26:26 -0400 |
| parents | b1fead9f68f2 |
| children | f38a3af9dd17 |
comparison
equal
deleted
inserted
replaced
| 464:e53d051681b0 | 465:4320c1a967c2 |
|---|---|
| 120 | 120 |
| 121 (* begin thide *) | 121 (* begin thide *) |
| 122 Definition fixDenote (T : Type) (dt : datatype) := | 122 Definition fixDenote (T : Type) (dt : datatype) := |
| 123 forall (R : Type), datatypeDenote R dt -> (T -> R). | 123 forall (R : Type), datatypeDenote R dt -> (T -> R). |
| 124 | 124 |
| 125 (** The idea of a recursion scheme is parameterized by a type and a reputed encoding of it. The principle itself is polymorphic in a type [R], which is the return type of the recursive function that we mean to write. The next argument is a hetergeneous list of one case of the recursive function definition for each datatype constructor. The [datatypeDenote] function turns out to have just the right definition to express the type we need; a set of function cases is just like an alternate set of constructors where we replace the original type [T] with the function result type [R]. Given such a reified definition, a [fixDenote] invocation returns a function from [T] to [R], which is just what we wanted. | 125 (** The idea of a recursion scheme is parameterized by a type and a reputed encoding of it. The principle itself is polymorphic in a type [R], which is the return type of the recursive function that we mean to write. The next argument is a heterogeneous list of one case of the recursive function definition for each datatype constructor. The [datatypeDenote] function turns out to have just the right definition to express the type we need; a set of function cases is just like an alternate set of constructors where we replace the original type [T] with the function result type [R]. Given such a reified definition, a [fixDenote] invocation returns a function from [T] to [R], which is just what we wanted. |
| 126 | 126 |
| 127 We are ready to write some example functions now. It will be useful to use one new function from the [DepList] library included in the book source. *) | 127 We are ready to write some example functions now. It will be useful to use one new function from the [DepList] library included in the book source. *) |
| 128 | 128 |
| 129 Check hmake. | 129 Check hmake. |
| 130 (** %\vspace{-.15in}% [[ | 130 (** %\vspace{-.15in}% [[ |