[Agda] Small Kernel

[Jesper Cockx]

Hi Peter,

Interesting.  Would it be right to say that coverage checking
> is simple in comparison to termination checking
> (which is after all undecidable, in principle)?
>

In general, coverage checking is just as undecidable as termination
checking, because it requires checking emptiness of a given type to
determine whether a case can be omitted. Agda uses inaccessible patterns to
recover a decidable fragment of coverage, which is similar to using a
particular criterion for termination like structural descent or size-change
termination.

This brought something to mind. With many datatypes (not codata) there
> is a canonical eliminator. You could press a button to have it
> generated and type-checked for you.  (This might even be useful).
> Imaginably, you might also get the canonical anamorphism from
> a declaration of codata; or even fancier gadgetry.


It should be possible to use Agda's reflection machinery to write a macro
that automatically generates the eliminator for a given datatype (in a
certain subset of all datatypes supported by Agda), and similarly you could
generate general principles to work with coinductive types like you mention.

A masochist or an idiot or a compiler from user syntax
> might try to write all programs using just these canonical
> eliminators as the only source of structural induction and/or recursion,
> even
> case-splits.


The translation from dependent pattern matching to eliminators is automated
in the Equations plugin for Coq, so there is no need for masochism. A true
masochist could try to reimplement Equations as an Agda macro. Personally I
would be more interested to do such a project using a type-safe reflection
interface such as levitation. But even with such an automatic translation,
I would suspect that you still want to keep around the case tree
representation of the function, for efficient evaluation if nothing else.

It seems that there is something like ex-falso-quodlibet
> lurking in the corners of full pattern matching.


It makes use of the conflict rule from Conor's "constructions on
constructors" to eliminate impossible cases, is this what you meant?

-- Jesper

On Thu, Dec 5, 2019 at 2:25 PM Peter Hancock <hancock at fastmail.fm> wrote:

> On 04/12/2019 09:13, Jesper Cockx wrote:
>
> > However, this story is far from complete because it takes the signature
> of
> > defined types and functions for granted. In particular, functions by
> > dependent pattern matching are represented as case trees that need to
> pass
> > coverage checking and termination checking, which means those checks are
> > also part of Agda's 'trusted core'.
>
> Interesting.  Would it be right to say that coverage checking
> is simple in comparison to termination checking
> (which is after all undecidable, in principle)?
>
> This brought something to mind. With many datatypes (not codata) there
> is a canonical eliminator. You could press a button to have it
> generated and type-checked for you.  (This might even be useful).
> Imaginably, you might also get the canonical anamorphism from
> a declaration of codata; or even fancier gadgetry.
>
> A masochist or an idiot or a compiler from user syntax
> might try to write all programs using just these canonical
> eliminators as the only source of structural induction and/or recursion,
> even
> case-splits.  That might be something like a core language, or
> imaginable (if sometimes nasty/prolix) "assembly code".
>
> One advantage of full pattern matching is avoiding
> programs with piles of deeply nested case distinctions.
> An example is a proof of transitivity, where
> pattern matching allows
>
>     tr tr' : (a b c : fm) -> Tr a b c
>     tr in0 in0 in0 in0* = id
>     tr (inS z) (inS z') (inS z'') (inS* z z' ab) (inS* z' z'' bc)
>      = inS* z z'' (tr z z' z'' ab bc)
>
> The (20 line) proof using just canonical eliminators took me
> horribly many hours to figure out. It is computationally horrible.
> It works only because the last clause of Tr is an equation.
>
> It seems that there is something like ex-falso-quodlibet
> lurking in the corners of full pattern matching.
> To be in a core-language, I wonder if it should be spelled
> out by explicitly using a boolean universe, or something ...
>
> Hank
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191205/00cf56e2/attachment.html>