[Agda] Small Kernel

[selinger at mathstat.dal.ca]

Hi Peter,

most of your questions are answered in the paper "Eliminating
Dependent Pattern Matching" by Goguen, McBride, and McKinna. The paper
explains how to translate programs that are defined by recursion and
full pattern matching into a core language using only induction
principles (i.e., canonical eliminators, which can be generated from
datatype definitions). It also explains why adding inaccessible
patterns makes (a certain fragement of) coverage decidable.

-- Peter

Peter Hancock 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
>