<br><br><div class="gmail_quote">2009/9/9 Stefan Holdermans <span dir="ltr"><<a href="mailto:stefan@cs.uu.nl">stefan@cs.uu.nl</a>></span><br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Dear Martin,<div class="im"><br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
By "black-holing" you probably mean co-induction. That is,<br>
if the statement to proven appears again, we assume it must hold.<br>
However, type classes are by default inductive, so there's no<br>
easy fix to offer to your problem.<br>
</blockquote>
<br></div>
A propos: are there fundamental objections to coinductive resolving, i.e., constructing recursive dictionaries. I suppose termination is hard to guarantee then: is it enough to require constraints to be productive w.r.t. instance heads?<br>
<font color="#888888"><br></font></blockquote><div><br>Yes, you need instances to be productive, otherwise, you get<br>bogus cyclic proofs like<br>instance Foo a => Foo a<br><br>dictFooa = dictFooa<br><br>You could call this a bug, or simply blame the programmer<br>
for writing down a 'bogus' instance.<br><br>Under co-inductive type class solving more (type class) programs will terminate (my guess). Here are some references:<br><br>Satish R. Thatte:
Semantics of Type Classes Revisited.
<a href="http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94" target="_blank">LISP and Functional Programming 1994</a>: 208-219<br><br>As far as I know, the first paper which talks about co-induction and type classes.<br>
<br>I myself and some co-workers explored this idea further in some<br>unpublished draft:<br><br><pre> AUTHOR = {M. Sulzmann and J. Wazny and P. J. Stuckey},<br> TITLE = {Co-induction and Type Improvement in Type Class Proofs},<br>
<br> NOTE = {Manuscript},<br> YEAR = {2005},<br> MONTH = {July},<br> PS = {<a href="http://www.cs.mu.oz.au/%7Esulzmann/manuscript/coind-type-class-proofs.ps" target="_blank">http://www.cs.mu.oz.au/~sulzmann/manuscript/coind-type-class-proofs.ps</a>}<br>
<br></pre><br>I'm quite fond of co-induction because it's such an elegant and powerful<br>proof technique. However, GHC's co-induction mechanism is fairly limited,<br>see Simon's reply, so I'm also curious to see what's happening in the future.<br>
<br>-Martin <br></div></div><br>