The Coq mailing list

[Carsten Schuermann <carsten AT cs.yale.edu>]

Dear Conor, Bruno, Dmitri, and all:

This discussion reminds me very much of my own observations when I
started my work on dependently typed programming for LF (Twelf), which
has led to the programming language Delphin.  There we had the same
problem.  Case analysis on individual variables didn't seem to make
much sense, because they might occur elsewhere as indices to other
types.

In our solution we generalize case analysis to work on entire contexts
instead of just individual variables.  Patterns are not individual
expressions but substitutions --- lists of expressions --- that describe
possible forms of contexts. 

Let's go back to the example from the previous mails --- removal of
the last element of a list.  In Twelf you define natural numbers and
lists (indexed by their length) as follows.  In Coq, this would
correspond to the definition of two datatypes.

  nat : type.
  z: nat.
  s: nat -> nat.

  list : nat -> type.
  nil : list z.
  cons : nat  -> list N -> list (s N).

In Delphin (whose implementation is still underway, draft paper on my
homepage), it is quite easy to write out the remove function without
any pred relation. Instead of pred, we simply pattern match.

remove :: All {N:nat} All {L1:list (s N)} Ex [L2:list N] True
fun remove (s N1) (cons H L) = let
                                  val <L', <>> =  remove N1 L
                               in
                                 <cons H L', <>>
                               end
  | remove z (cons H nil) = <nil, <>>


What is going on under the hood is pretty straight forward.  A case
statement takes a list of triplets as arguments, each triplet stands for
a case.  There is no need for a case subject, because the operational
semantics will always match against the entire context in which case is
defined.


        case [(G1; s1; P1), ..., (Gn; sn; Pn)]

(G1 .. Gn are contexts, s1 .. sn are patterns (or alternatively
substitutions), and P1 ... Pn are the bodies of the individual cases)


The typing rule for this case is as follows.  We write G |- P : T
for "program P has type T", and G |- s : G' for "substitution 
s has domain G', and is well typed in G."

        Gi |- si : G      Gi |- Pi : T[si]        for all i
        ===================================================
        G |- case [(G1; s1; P1), ..., (Gn; sn; Pn)] : T

The reduction rule with explicit environment is also simple.
(the o is substitution composition and the ====> the big
step operational semantics)


        eta = si o eta'    eta' |- Pi ====> V      for some i
        ======================================================
        eta |- case [(G1; s1; P1), ..., (Gn; sn; Pn)] ====> V



Back to the example.  The case analysis for the remove function is
defined in context

        N:nat, L1: list N.

In this notation the case statement has the form

        case  [(N1:nat, H:nat, L:nat; 
                (s N1)/N, (cons H L)/L1;
                ....),
               (z:nat, H:nat;
                z/N, (cons H nil)/L1;
                ....)]

The trick of thinking of patterns as substitutions has solved all my
problems, and I think it is a quite natural generalization of the
typical case construct in programming languages or proof assistants.
Can this idea also be adopted for Coq?

Best,
-- Carsten



 
On Fri, 2002-09-13 at 07:19, C T McBride wrote:
> Hello all
> 
> This problem touches on a number of issues relating to technology,
> technique and taste. When programming with dependent types, I have
often
> taken too long to ask myself `is this the right problem?' and `are
these
> the right tools?' as well as `how do I get this to work?'. 
> 
> 
> Dmitri Hendricks wrote:
> 
> > Does anyone know how to solve the following
easy-to-formulate-problem.
> 
> > I want to define a function which removes the last element of a
> > tuple. Tuples are defined as generalized pairs; a tuple of n
> > A-elements is of type (cp A n), the cartesian product of n copies of
> > set A and the unit set, defined by:
> 
> > Fixpoint cp [A:Set;n:nat] : Set :=
> > Cases n of
> > | O    => unit
> > |(S m) => A*(cp A m)
> > end.
> 
> First, note that this is but one way to define `vectors'. One can also
> define them functionally as (Fin n)->A (where (Fin n) is a type with n
> canonical elements) or inductively (listn in the Coq library?). Which
> is the most convenient? It depends on the job you want to do, but the
> inductive version is usually cleaner than the computed-tuple version,
> because dependent case analysis on the vector gives you case analysis
> on its length `for free'. Further, few implicit syntax mechanisms are
> smart enough to spot that (A * A * A * unit) is (cp A 3), whereas
> (listn A 3) is obviously a vector of length 3. However, for the task
> here, it doesn't really matter which you choose.
> 
> Now, what is the type of `removing the last'? I have no idea how to
> remove the last element of an empty vector, so I'd choose the type
> 
>   rm_last : (A:Set)(n:nat)(cp A (S n))->(cp A n)
> 
> With this type, rm_last is a straightforward fix-and-case,
corresponding
> to
> 
>   rm_last A  O     _     => void
>   rm_last A (S n) (x,xs) => (x,rm_last xs)
> 
> Furthermore, its safe usage in programs requires no awkward reasoning
> about properties of the pred function...
> 
> ...which brings me to the next point: the pred function has very bad
> properties---the dummy return value for 0 complicates every program
which
> uses it, especially if it appears in a type. Dependently typed
programming
> makes partial functions harder to cope with, but easier to avoid!
> Most forms of subtraction (in the absence of negatives) are just
impolite.
> 
> That said, if pred 0 = 0, then there's an obvious dummy value which
> rm_last must return for empty vectors. Now, Dmitri says
> 
> > In order to compute the type of the tuple obtained by the removal of
> > its last element, I need the function pred', which (in contrast to
pred)
> > removes the innermost S of a natural number:
> 
> In fact, that's not the case and only makes the problem harder. It
works
> ok to use the ordinary pred (if it's the obvious pred defined with
case,
> stripping off the outer S). We may write the equivalent of
> 
>   rm_last_bad : (A:Set)(n:nat)(cp A n)->(cp A (pred n))
>   rm_last_bad A  O    x => void
>   rm_last_bad A (S m) x => rm_last A m x
> 
> where rm_last is the version described above. Note that in the S case,
> the type of x is (cp A (S m)) and the return type is (cp A m) because
> (pred (S m)) is m.
> 
> Meanwhile, am I right in saying that the problem in defining the
> complicated pred' and its associated complicated rm_last arise from
> the syntactic guardedness condition for fixpoints? Whilst awaiting
> more a robust solution based on subtyping, I can recommend the
> memoization technique Eduardo uses in his TYPES 94 paper (showing that
> the syntactic check is sound). I used a variation of it in my thesis,
> and found it was fairly easy to work with.
> 
> Bruno Barras comments:
> 
> > I'd say this example raises an interesting question about typing
> > Cases. It shows that we may want to have the choice between
> > dependent and non-dependent elimination for each branch, and not
> > only for a given Case expression...
> 
> Why don't we just use dependent elimination for everything?
> 
> More fundamentally, good support for dependently typed programming
> requires that the case expression---as a programming notation if not
> as an underlying computational mechanism---be discarded altogether.
> The reason is simple. If we are writing a program with some type
> 
>   (x:X)(y:Y)(z:Z)W
> 
> and we do case analysis on y, the effect is not just to fill in
> constructor patterns for y; potentially, Z and W will become more
> specific, and potentially, x will also be instantiated with patterns
> (not necessarily made from constructors). Case analysis on one pattern
> variable thus has non-local effects on types and other pattern
variables
> which the conventional `column of patterns' cannot capture.
> 
> The point, once again, is that dependently typed programming is not
> just normal functional programming with more complicated
> types. Dependent types ask more radical questions: `What is a suitable
> programming language?', `What are suitable programming tools?' and
> most importantly `What are suitable programs?'. Even examples such as
> rm_last show us how much thinking we still must do.
> 
> I'll stop beating my drum now...
> 
> Cheers
> 
> Conor
> 
> 
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club