<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On 7 Oct 2010, at 22:19, Andreas Abel wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>Ok, this works, but anyway, I think inductive records are doomed.<br><br>Eta-expansion does not terminate for inductive record like List so I guess there will be soon a check to rule them out.<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div>I hope not. As I have said it is very strange not to be allowed to use records in recursive definitions.</div><div><br></div><div>I'd rather get rid of eta equality.</div><div><br></div><div>Thorsten</div><div><div><br></div><br><blockquote type="cite"><div>On Oct 6, 2010, at 10:41 PM, Nicolas Pouillard wrote:<br><br><blockquote type="cite">On Wed, 6 Oct 2010 11:03:08 +0200, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>> wrote:<br></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">On Oct 5, 2010, at 5:29 PM, Nils Anders Danielsson wrote:<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">On 2010-10-05 14:14, Andreas Abel wrote:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">Currently records are hybrids, because we have record patterns. If<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">all<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">record patterns could be translated away, we could understand<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">records in<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">terms of &. But currently we allow record patterns that cannot be<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">translated away, such as where record patterns are mixed with data<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">constructor patterns.<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">I'm fairly certain that we can translate away these patterns, but<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">there<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">is no immediate need to do so, because the translation would be<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">observationally indistinguishable from what we generate now (modulo<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">any<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">bugs).<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">How would you translate away the patterns in Thorsten's example?<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">record List (A : Set) : Set where<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> constructor list<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> field<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> isCons : Bool<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> hd : T isCons → A<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> tl : T isCons → List A<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">append : ∀ {A} → List A → List A → List A<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">append (list true h t) bs = list true h (λ _ → append (t _) bs)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">append (list false _ _) bs = bs<br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">[...]<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><blockquote type="cite">Anyway, for now the termination checker rejects all versions of append<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">given here, shout if you disagree!<br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">One may consider this as cheating but by boxing the recursive occurence<br></blockquote><blockquote type="cite">of (List A) one can please the termination checker:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">data Box (A : Set) : Set where<br></blockquote><blockquote type="cite"> box : A → Box A<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">record List (A : Set) : Set where<br></blockquote><blockquote type="cite"> constructor list<br></blockquote><blockquote type="cite"> field<br></blockquote><blockquote type="cite"> isCons : Bool<br></blockquote><blockquote type="cite"> hd : T isCons → A<br></blockquote><blockquote type="cite"> tl : T isCons → Box (List A)<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">open List<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">append : ∀ {A} → List A → List A → List A<br></blockquote><blockquote type="cite">append l bs with isCons l | hd l | tl l<br></blockquote><blockquote type="cite">... | false | _ | _ = bs<br></blockquote><blockquote type="cite">... | true | h | t with t _<br></blockquote><blockquote type="cite">... | box t' = list true h (λ _ → box (append t' bs))<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">By replacing Box by ∞ one get CoList.<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">Best regards,<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">-- <br></blockquote><blockquote type="cite">Nicolas Pouillard<br></blockquote><blockquote type="cite"><a href="http://nicolaspouillard.fr">http://nicolaspouillard.fr</a><br></blockquote><blockquote type="cite"><br></blockquote><br>Andreas Abel <>< Du bist der geliebte Mensch.<br><br>Theoretical Computer Science, University of Munich<br>Oettingenstr. 67, D-80538 Munich, GERMANY<br><br><a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>http://www2.tcs.ifi.lmu.de/~abel/<br><br>_______________________________________________<br>Agda mailing list<br>Agda@lists.chalmers.se<br>https://lists.chalmers.se/mailman/listinfo/agda<br></div></blockquote></div><br></body></html>