<div dir="ltr">Hello everyone,<div><br></div><div>I&#39;ve actually implemented a little Agda-like clone with Francisco Ferreira called &quot;Ditto&quot; 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&#39;s problem, for example here is a little Ditto program that you can&#39;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 &quot;where did this goal come from?&quot; problem a little bit better.</div><div>I&#39;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">&lt;<a href="mailto:aaron-stump@uiowa.edu" target="_blank">aaron-stump@uiowa.edu</a>&gt;</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">&lt;<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>&gt;</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&#39;t have any
                        default cases, this would have the effect that
                        default cases aren&#39;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>