Mercurial > cpdt > repo
comparison src/Generic.v @ 395:3c941750c347
Citations for lazy data structures, Haskell 'deriving', and logic programming
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 22 Apr 2012 16:25:22 -0400 |
| parents | d1276004eec9 |
| children | 05efde66559d |
comparison
equal
deleted
inserted
replaced
| 394:cc8d0503619f | 395:3c941750c347 |
|---|---|
| 16 (* end hide *) | 16 (* end hide *) |
| 17 | 17 |
| 18 | 18 |
| 19 (** %\chapter{Generic Programming}% *) | 19 (** %\chapter{Generic Programming}% *) |
| 20 | 20 |
| 21 (** %\index{generic programming}\textit{%#<i>#Generic programming#</i>#%}% makes it possible to write functions that operate over different types of data. %\index{parametric polymorphism}%Parametric polymorphism in ML and Haskell is one of the simplest examples. ML-style %\index{module systems}%module systems%~\cite{modules}% and Haskell %\index{type classes}%type classes%~\cite{typeclasses}% are more flexible cases. These language features are often not as powerful as we would like. For instance, while Haskell includes a type class classifying those types whose values can be pretty-printed, per-type pretty-printing is usually either implemented manually or implemented via a %\index{deriving clauses}%[deriving] clause, which triggers ad-hoc code generation. Some clever encoding tricks have been used to achieve better within Haskell and other languages, but we can do %\index{datatype-generic programming}\emph{%#<i>#datatype-generic programming#</i>#%}% much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support. | 21 (** %\index{generic programming}\textit{%#<i>#Generic programming#</i>#%}% makes it possible to write functions that operate over different types of data. %\index{parametric polymorphism}%Parametric polymorphism in ML and Haskell is one of the simplest examples. ML-style %\index{module systems}%module systems%~\cite{modules}% and Haskell %\index{type classes}%type classes%~\cite{typeclasses}% are more flexible cases. These language features are often not as powerful as we would like. For instance, while Haskell includes a type class classifying those types whose values can be pretty-printed, per-type pretty-printing is usually either implemented manually or implemented via a %\index{deriving clauses}%[deriving] clause%~\cite{deriving}%, which triggers ad-hoc code generation. Some clever encoding tricks have been used to achieve better within Haskell and other languages, but we can do %\index{datatype-generic programming}\emph{%#<i>#datatype-generic programming#</i>#%}% much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support. |
| 22 | 22 |
| 23 Generic programming can often be very useful in Coq developments, so we devote this chapter to studying it. In a proof assistant, there is the new possibility of generic proofs about generic programs, which we also devote some space to. *) | 23 Generic programming can often be very useful in Coq developments, so we devote this chapter to studying it. In a proof assistant, there is the new possibility of generic proofs about generic programs, which we also devote some space to. *) |
| 24 | 24 |
| 25 (** * Reflecting Datatype Definitions *) | 25 (** * Reflecting Datatype Definitions *) |
| 26 | 26 |