[Agda] Reasoning with Pattern Match with Default Cases

[Larrytheliquid]

Hello everyone,

I've actually implemented a little Agda-like clone with Francisco Ferreira
called "Ditto" that does perform coverage checking before type checking,
available here:
https://github.com/ditto/ditto

This does indeed allows you to solve Marco's problem, for example here is a
little Ditto program that you can't write in Agda currently:
https://gist.github.com/larrytheliquid/80260b041c02c2a9e7b8

This can help to shrink the size of programs by quite a bit, for example
this blog post about logical relations runs into a program that needs to do
lots of default case splits:
http://blog.ezyang.com/2013/09/induction-and-logical-relations/

The one big drawback is that if you have holes, those holes get duplicated
across the coverings generated by the coverage checker.
For example, this file has more than 2 holes due to the coverings that get
generated:
https://github.com/ditto/ditto/blob/master/examples/stlc.dtt

Because of this, we allow users to name their holes, like in Idris, which
makes the "where did this goal come from?" problem a little bit better.
I'm still unsure about whether this is a good or bad solution, but it sure
does make programming some functions much nicer!

I think in an ideal world you could tell the system to generate coverings
before or after type checking, that you can chose when you need the extra
surface-language-level expressivity.

On Thu, Nov 12, 2015 at 3:01 PM, Aaron Stump <aaron-stump at uiowa.edu> wrote:

> I ran into this issue, too.  It would be interesting if Agda could keep
> track of the fact that certain patterns had not matched a given term -- but
> maybe not worth the additional complexity in theory and implementation.
> Aaron
>
>
> On 11/12/2015 03:38 PM, Ulf Norell wrote:
>
>
>
> On Thu, Nov 12, 2015 at 8:59 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
>
>> A way to improve how Agda handles these cases would be to do coverage
>> checking before type checking and only type checking the resulting case
>> tree. Since case trees don't have any default cases, this would have the
>> effect that default cases aren't typechecked themselves, but only their
>> expanded versions.
>>
>
> Actually, the case tree representation we use does have default cases.
>
> / Ulf
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>


-- 
Respectfully,
Larry Diehl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151112/b3cce136/attachment-0001.html