[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Conor McBride]

On 9 Jan 2014, at 00:14, Jesper Cockx <Jesper at sikanda.be> wrote:

> On Wed, Jan 8, 2014 at 9:41 PM, Conor McBride <conor at strictlypositive.org> wrote:
> 
> One reason why my brief career as a singer-songwriter was curtailed is that
> I could never remember the words, but I think it highly unlikely that the
> paper we wrote back then made any kind of assurance about mutual definitions
> like moo and noo. If I did, then perhaps I join the good company in error,
> for which I apologize.
> 
> I'm sorry, I meant the version of noo I gave in my previous mail. I'd better call it something else:
> 
> woo : (X : Set) -> (WOne <-> X) -> X -> Zero
> woo .WOne Refl (wrap f) = woo (Zero -> WOne) myIso f

That's fair enough.

> bad : Zero
> bad = woo WOne Refl (wrap \ ())
> 
> The definition of woo falls within the framework of EDPM. Moreover, it is structurally recursive on its third argument.

Given the definition of < there, it is indeed the case that the third
argument in the recursive call is smaller than the third argument on
the left-hand side.

> It is still incompatible with univalence (as shown by 'bad'), and it cannot be translated to eliminators.

Indeed it cannot, as the appeal to recursion can only be made once the
elimination of the equality has been matched, revealing a datatype
upon which to do recursion. Indeed there is an assumption (which is
made explicit in the proof of thm 24, but I agree should have been stated
earlier) that structural recursion is done on things in datatypes, and that
the datatype determines the notion of "structurally smaller". Correspondingly,
the definition of < should probably have been made more carefully, in a
typed way, avoiding the following

>  I quite agree that the definition of "structurally smaller" we gave does say
> that
> 
>   f < wrap f

which inadvertently allows a non-subobject to be considered "smaller". The
method appeals to recursion at the top level, then matching to reveal
subterms: it does not allow matching to reveal opportunities for recursion
not apparent at the top level.

> Of course, transporting a term along an equation should not preserve structural ordering. Yet we should still be able to pattern match on equality proofs (in the --without-K sense), as long as the definition can be translated to eliminators.

Sure. We just need to book-keep the inductive hypotheses, so that they too are
transformed by equality. Sometimes, that's very useful. Here, it carefully
preserves the uselessness of the inductive hypothesis.

> I agree, and I think neither should pattern matching let us do this (at least not with --without-K enabled). But wasn't the whole point of EDPM to show that it *is* safe to use pattern matching?

Technically, its purpose is to show that K (with computational behaviour) is
exactly (not just at least) the gap between eliminators and pattern matching.
Politically, the point is that "the technology for explaining pattern matching
and other programming language constructs is as important as the language
constructs themselves". And in my thesis, I am more explicit that we should
*not* consider pattern matching the primitive mode of definition, but rather
use eliminators to write programs which we can read in a pattern matching
style. By "eliminators", I mean not only those which come as standard equipment
with datatypes, but also those we can define, capturing whatever notions of
structural decomposition we care to justify.

> What Daniel and Thomas on the Coq list showed, is that we need an additional criterion for pattern matching to be safe. My proposal is to require that the type of the argument on which the function is structurally recursive, should be a data type.

Sounds about right: moreover that the notion of "structurally smaller" we
use should be induced by that datatype, and thus accounted for by, say,
course-of-values memoization for that type.

> A different (and probably much more sophisticated) proposal was given on the Coq list. Do you have another proposal?

I'm not in the business of proposing fragments of pattern matching that we
can certify as safe and set in stone. Given that dependent types can describe
case analyses and recursion schemes for data, I think we should use them as
the language for characterizing what we think makes sense. If we have to use
some other criteria on top of types to divide sense from nonsense, we're
missing something.

> On the long term, I think the best way to go would be to actually perform the translation of pattern matching to eliminators in Agda, similar to Matthieu's Equations plugin for Coq. There are just too many subtleties to pattern matching to get everything correct otherwise, especially when univalence and higher inductives are involved.

I agree, and I'd add that in the interactive setting, eliminators describe
incremental steps of constructing a function in the first place. That's what
James McKinna and I did in the definition of Epigram. The analogue of Agda's
[C-c C-c] case-split was delivered by invoking an eliminator (any eliminator,
not just constructor case analysis) and reporting the subgoals in a syntax
which looked like the left-hand sides of programs. Now it's clear that with
every elimination made explicit, programs can get clunky quite quickly, so
it might be nice to infer unremarkable case analysis trees from constructor
patterns, but that's fancy elaboration technology outside the kernel. The
present situation in both Agda and Coq is to hardwire kernel-level support
for what seem to be the common cases, without entirely checking that
everything is ok.

I'd be even happier with type-based systems for recursion which bring
the recursively defined symbols into scope at types which exactly describe
their permitted uses, without the need for a separate check. What's important
is that type checking is enough to establish the status of terms as evidence.

All the best

Conor