<div dir="ltr"><div><div><div>The point of termination checker is roughly to "desugar" recursive definitions with pattern matching into non-recursive definitions that use universal eliminator.<br>(I think it's not quite what it does in Agda, but that's how its behavior is justified).<br><br></div>Here you have no pattern matching so there's nothing to desugar, so nothing for termination checker to do.<br></div>When you write something using universal eliminators, that's normally an exercise in avoiding recursion altogether.<br><br>> 
<span style="text-align:start;text-indent:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">so obvious cases</span></span>

<br></div><div>It's not so obvious: you need to know that [fold] will only ever give you "smaller" 
<font face="monospace, monospace">ξs<span style="font-family:arial,helvetica,sans-serif">, which is maybe possible using sized types (I have no idea), but it's not visible syntactically in the definition of [zip-with].</span></font><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 17 February 2018 at 09:37, v0ιd <span dir="ltr"><<a href="mailto:igorzsci@gmail.com" target="_blank">igorzsci@gmail.com</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>Dear list,</div><div>I try to define a zip-with function without pattern matching through universal constructor eliminator for Lists.</div><div><br></div><div><div><font face="monospace, monospace">

<span style="color:rgb(34,34,34);font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">id</span> : {a : _} → {A : Set a} → A → A</font></div><div><font face="monospace, monospace">

<span style="color:rgb(34,34,34);font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">id</span> x = x</font></div></div><div><font face="monospace, monospace"><br></font></div><div><div><font face="monospace, monospace">data List {a} (A : Set a) : Set a where</font></div><div><font face="monospace, monospace"> nil : List A</font></div><div><font face="monospace, monospace"> cons : A → List A → List A</font></div><div><font face="monospace, monospace"><br></font></div><div><div><font face="monospace, monospace">fold : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → List A → (A → List A → ((B → C) → B → C) → (B → C) → B → C) → (B → C) → B → C</font></div><div><font face="monospace, monospace">fold nil _ fs s = fs s</font></div><div><font face="monospace, monospace">fold (cons x xs) f = f x xs (fold xs f)</font></div></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">zip-with : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → (A → B → C) → List A → List B → List C</font></div></div><div><div><font face="monospace, monospace">zip-with f x y = fold x (λ ξ ξs _ _ _ → fold y (λ η ηs _ _ _ → cons (f ξ η) (zip-with f ξs ηs)) id nil) id nil</font></div></div><div><br></div><div>

<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">But it fails termination checking.</span><br></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><br></span></div><div><span style="text-align:start;text-indent:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><div><font face="monospace, monospace">Termination checking failed for the following functions:</font></div><div><font face="monospace, monospace">  zip-with</font></div><div><font face="monospace, monospace">Problematic calls:</font></div><div><font face="monospace, monospace">  zip-with f ξs ηs</font></div><div><br></div><div>I would not want to suppress <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">termination checking at all with {-# TERMINATING #-}.</span></div><div>What can I do here? Maybe it makes sense somehow to improve <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">termination checker for so obvious cases?</span></div></span></div></div>
<br>______________________________<wbr>_________________<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/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>