Mercurial > cpdt > repo
changeset 107:924d77a177e8
hlist and hget
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 13 Oct 2008 12:35:48 -0400 |
parents | 1d2746eae1a6 |
children | 7abf5535baab |
files | src/DataStruct.v |
diffstat | 1 files changed, 55 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/src/DataStruct.v Mon Oct 13 11:59:20 2008 -0400 +++ b/src/DataStruct.v Mon Oct 13 12:35:48 2008 -0400 @@ -115,6 +115,8 @@ Implicit Arguments Nil [A]. +(** Our [get] function is quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *) + Section ilist_map. Variables A B : Set. Variable f : A -> B. @@ -125,12 +127,59 @@ | Cons _ x ls' => Cons (f x) (imap ls') end. - Theorem get_imap : forall n (ls : ilist A n) (idx : index n), + (** It is easy to prove that [get] "distributes over" [imap] calls. The only tricky bit is remembering to use the [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *) + + Theorem get_imap : forall n (idx : index n) (ls : ilist A n), get (imap ls) idx = f (get ls idx). - induction ls; crush; - match goal with - | [ |- context[match ?IDX with First _ => _ | Next _ _ => _ end] ] => - dep_destruct IDX; crush - end. + induction ls; dep_destruct idx; crush. Qed. End ilist_map. + + +(** * Heterogeneous Lists *) + +(** Programmers who move to statically-typed functional languages from "scripting languages" often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a "type-level" list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and it we can do it much more cleanly and directly in Coq. *) + +Section hlist. + Variable A : Type. + Variable B : A -> Type. + + (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *) + + Inductive hlist : list A -> Type := + | MNil : hlist nil + | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). + + (** We can implement a variant of the last section's [get] function for [hlist]s. To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to. *) + + Variable elm : A. + + Inductive member : list A -> Type := + | MFirst : forall ls, member (elm :: ls) + | MNext : forall x ls, member ls -> member (x :: ls). + + (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable. In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too. The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations. + + We can use [member] to adapt our definition of [get] to [hlists]. The same basic [match] tricks apply. In the [MCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match]. We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *) + + Fixpoint hget ls (mls : hlist ls) {struct mls} : member ls -> B elm := + match mls in hlist ls return member ls -> B elm with + | MNil => fun mem => + match mem in member ls' return (match ls' with + | nil => B elm + | _ :: _ => unit + end) with + | MFirst _ => tt + | MNext _ _ _ => tt + end + | MCons _ _ x mls' => fun mem => + match mem in member ls' return (match ls' with + | nil => Empty_set + | x' :: ls'' => + B x' -> (member ls'' -> B elm) -> B elm + end) with + | MFirst _ => fun x _ => x + | MNext _ _ mem' => fun _ get_mls' => get_mls' mem' + end x (hget mls') + end. +End hlist.