The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Edsko

On 9 Jun 2008, at 15:45, Edsko de Vries wrote:

> On Mon, Jun 09, 2008 at 03:25:05PM +0100, Conor McBride wrote:
> > Let's be clear: this is a fact about Coq, not
> > about vectors.
>
> Can I ask a question about that? I'll readily admit that in Epigram or
> Agda the code for vectors and the code for tuples would be equally
> simple, whereas in Coq the code for vectors would be relatively
> complicated. The way I understand it though is that the simple code I
> write in Epigram is translated internally into something that would
> probably resemble the code I write in Coq (at least conceptually).

That's true, up to a point. Moreover, the
translation happens incrementally and drives
the whole interactive process.

> Can
> this complexity always be hidden?

We're quite systematic about hiding it. There's
no need for programmers to be exposed to the
details of the translation (although the
editor's display of contextual information
could have been tidier in this respect).

Crucially, (hence the "up to a point") it's a
bidirectional translation. Translated values
carry extra information that you might not think
of writing in Coq (although there's nothing to
stop you). This information describes the
high-level programs to which low-level terms
correspond. It is suitably preserved by
computation, so the machine can read off simple
code from the result of computing with its ugly
translation.

> Suppose I want to do proofs over my
> functions later on, will this "hidden complexity" never come back to
> bite me?

If you write ordinary pattern matching programs,
then no. If you use hand-rolled elimination operators,
you may find situations where we hide too much:
there's certainly more to say and more work to do
there.

All the best

Conor