The Coq mailing list

[C T McBride <c.t.mcbride AT durham.ac.uk>]

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