comparison src/MoreDep.v @ 484:5025a401ad9e

Last round of feedback from class at Penn
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 Jan 2013 16:23:26 -0500
parents f38a3af9dd17
children 2d7ce9e011f4
comparison
equal deleted inserted replaced
483:582cf453878e 484:5025a401ad9e
58 58
59 (** Using [return] alone allowed us to express a dependency of the [match] result type on the _value_ of the discriminee. What %\index{Gallina terms!in}%[in] adds to our arsenal is a way of expressing a dependency on the _type_ of the discriminee. Specifically, the [n1] in the [in] clause above is a _binding occurrence_ whose scope is the [return] clause. 59 (** Using [return] alone allowed us to express a dependency of the [match] result type on the _value_ of the discriminee. What %\index{Gallina terms!in}%[in] adds to our arsenal is a way of expressing a dependency on the _type_ of the discriminee. Specifically, the [n1] in the [in] clause above is a _binding occurrence_ whose scope is the [return] clause.
60 60
61 We may use [in] clauses only to bind names for the arguments of an inductive type family. That is, each [in] clause must be an inductive type family name applied to a sequence of underscores and variable names of the proper length. The positions for _parameters_ to the type family must all be underscores. Parameters are those arguments declared with section variables or with entries to the left of the first colon in an inductive definition. They cannot vary depending on which constructor was used to build the discriminee, so Coq prohibits pointless matches on them. It is those arguments defined in the type to the right of the colon that we may name with [in] clauses. 61 We may use [in] clauses only to bind names for the arguments of an inductive type family. That is, each [in] clause must be an inductive type family name applied to a sequence of underscores and variable names of the proper length. The positions for _parameters_ to the type family must all be underscores. Parameters are those arguments declared with section variables or with entries to the left of the first colon in an inductive definition. They cannot vary depending on which constructor was used to build the discriminee, so Coq prohibits pointless matches on them. It is those arguments defined in the type to the right of the colon that we may name with [in] clauses.
62 62
63 Our [app] function could be typed in so-called%\index{stratified type systems}% _stratified_ type systems, which avoid true dependency. That is, we could consider the length indices to lists to live in a separate, compile-time-only universe from the lists themselves. Compile-time data may be _erased_ such that we can still execute a program. As an example where erasure would not work, consider an injection function from regular lists to length-indexed lists. Here the run-time computation actually depends on details of the compile-time argument, if we decide that the list to inject can be considered compile-time. More commonly, we think of lists as run-time data. Neither case will work with %\%naive erasure. (It is not too important to grasp the details of this run-time/compile-time distinction, since Coq's expressive power comes from avoiding such restrictions.) *) 63 Our [app] function could be typed in so-called%\index{stratified type systems}% _stratified_ type systems, which avoid true dependency. That is, we could consider the length indices to lists to live in a separate, compile-time-only universe from the lists themselves. Compile-time data may be _erased_ such that we can still execute a program. As an example where erasure would not work, consider an injection function from regular lists to length-indexed lists. Here the run-time computation actually depends on details of the compile-time argument, if we decide that the list to inject can be considered compile-time. More commonly, we think of lists as run-time data. Neither case will work with %\%naive%{}% erasure. (It is not too important to grasp the details of this run-time/compile-time distinction, since Coq's expressive power comes from avoiding such restrictions.) *)
64 64
65 (* EX: Implement injection from normal lists *) 65 (* EX: Implement injection from normal lists *)
66 66
67 (* begin thide *) 67 (* begin thide *)
68 Fixpoint inject (ls : list A) : ilist (length ls) := 68 Fixpoint inject (ls : list A) : ilist (length ls) :=