## Mercurial > cpdt > repo

### comparison src/Generic.v @ 480:f38a3af9dd17

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Batch of changes based on proofreader feedback

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Fri, 30 Nov 2012 11:57:55 -0500 |

parents | 4320c1a967c2 |

children | 31258618ef73 |

comparison

equal
deleted
inserted
replaced

479:40a9a36844d6 | 480:f38a3af9dd17 |
---|---|

28 | 28 |

29 (** The key to generic programming with dependent types is%\index{universe types}% _universe types_. This concept should not be confused with the idea of _universes_ from the metatheory of CIC and related languages. Rather, the idea of universe types is to define inductive types that provide _syntactic representations_ of Coq types. We cannot directly write CIC programs that do case analysis on types, but we _can_ case analyze on reified syntactic versions of those types. | 29 (** The key to generic programming with dependent types is%\index{universe types}% _universe types_. This concept should not be confused with the idea of _universes_ from the metatheory of CIC and related languages. Rather, the idea of universe types is to define inductive types that provide _syntactic representations_ of Coq types. We cannot directly write CIC programs that do case analysis on types, but we _can_ case analyze on reified syntactic versions of those types. |

30 | 30 |

31 Thus, to begin, we must define a syntactic representation of some class of datatypes. In this chapter, our running example will have to do with basic algebraic datatypes, of the kind found in ML and Haskell, but without additional bells and whistles like type parameters and mutually recursive definitions. | 31 Thus, to begin, we must define a syntactic representation of some class of datatypes. In this chapter, our running example will have to do with basic algebraic datatypes, of the kind found in ML and Haskell, but without additional bells and whistles like type parameters and mutually recursive definitions. |

32 | 32 |

33 The first step is to define a representation for constructors of our datatypes. *) | 33 The first step is to define a representation for constructors of our datatypes. We use the [Record] command as a shorthand for defining an inductive type with a single constructor, plus projection functions for pulling out any of the named arguments to that constructor. *) |

34 | 34 |

35 (* EX: Define a reified representation of simple algebraic datatypes. *) | 35 (* EX: Define a reified representation of simple algebraic datatypes. *) |

36 | 36 |

37 (* begin thide *) | 37 (* begin thide *) |

38 Record constructor : Type := Con { | 38 Record constructor : Type := Con { |

40 recursive : nat | 40 recursive : nat |

41 }. | 41 }. |

42 | 42 |

43 (** The idea is that a constructor represented as [Con T n] has [n] arguments of the type that we are defining. Additionally, all of the other, non-recursive arguments can be encoded in the type [T]. When there are no non-recursive arguments, [T] can be [unit]. When there are two non-recursive arguments, of types [A] and [B], [T] can be [A * B]. We can generalize to any number of arguments via tupling. | 43 (** The idea is that a constructor represented as [Con T n] has [n] arguments of the type that we are defining. Additionally, all of the other, non-recursive arguments can be encoded in the type [T]. When there are no non-recursive arguments, [T] can be [unit]. When there are two non-recursive arguments, of types [A] and [B], [T] can be [A * B]. We can generalize to any number of arguments via tupling. |

44 | 44 |

45 With this definition, it as easy to define a datatype representation in terms of lists of constructors. *) | 45 With this definition, it is easy to define a datatype representation in terms of lists of constructors. The intended meaning is that the datatype came from an inductive definition including exactly the constructors in the list. *) |

46 | 46 |

47 Definition datatype := list constructor. | 47 Definition datatype := list constructor. |

48 | 48 |

49 (** Here are a few example encodings for some common types from the Coq standard library. While our syntax type does not support type parameters directly, we can implement them at the meta level, via functions from types to [datatype]s. *) | 49 (** Here are a few example encodings for some common types from the Coq standard library. While our syntax type does not support type parameters directly, we can implement them at the meta level, via functions from types to [datatype]s. *) |

50 | 50 |