<div dir="ltr">Hello everyone,<div><br></div><div>I've actually implemented a little Agda-like clone with Francisco Ferreira called "Ditto" that does perform coverage checking before type checking, available here:</div><div><a href="https://github.com/ditto/ditto">https://github.com/ditto/ditto</a><br></div><div><br></div><div>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:</div><div><a href="https://gist.github.com/larrytheliquid/80260b041c02c2a9e7b8">https://gist.github.com/larrytheliquid/80260b041c02c2a9e7b8</a><br></div><div><br></div><div>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:</div><div><a href="http://blog.ezyang.com/2013/09/induction-and-logical-relations/">http://blog.ezyang.com/2013/09/induction-and-logical-relations/</a><br></div><div><br></div><div>The one big drawback is that if you have holes, those holes get duplicated across the coverings generated by the coverage checker.</div><div>For example, this file has more than 2 holes due to the coverings that get generated:</div><div><a href="https://github.com/ditto/ditto/blob/master/examples/stlc.dtt">https://github.com/ditto/ditto/blob/master/examples/stlc.dtt</a><br></div><div><br></div><div>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.</div><div>I'm still unsure about whether this is a good or bad solution, but it sure does make programming some functions much nicer!</div><div><br></div><div>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. </div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 12, 2015 at 3:01 PM, Aaron Stump <span dir="ltr"><<a href="mailto:aaron-stump@uiowa.edu" target="_blank">aaron-stump@uiowa.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
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.<span class="HOEnZb"><font color="#888888"><br>
Aaron</font></span><div><div class="h5"><br>
<br>
<div>On 11/12/2015 03:38 PM, Ulf Norell
wrote:<br>
</div>
</div></div><blockquote type="cite"><div><div class="h5">
<div dir="ltr"><br>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Thu, Nov 12, 2015 at 8:59 PM,
Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">
<div>
<div>
<div>
<div>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.</div>
</div>
</div>
</div>
</div>
</blockquote>
<div><br>
</div>
<div>Actually, the case tree representation we use does have
default cases.</div>
<div><br>
</div>
<div>/ Ulf</div>
</div>
</div>
</div>
<br>
<fieldset></fieldset>
<br>
</div></div><span class=""><pre>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</span></blockquote>
<br>
</div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature">Respectfully,<br>Larry Diehl<br></div>
</div>