[Agda] Small Kernel

[Peter Hancock]

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