<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<tt>Do you need the recursive call? I started implementing the same<br>
function using Vec instead of List to make the size invariant<br>
clearer and after a bit of cleaning up I got an implementation<br>
which is just using two folds (which makes sense: the first one<br>
performs the induction, the second one is merely used to do a<br>
case analysis)<br>
<br>
</tt><tt><tt>================================================================<br>
</tt>open import Agda.Builtin.Nat<br>
<br>
id : {a : _} → {A : Set a} → A → A<br>
id x = x<br>
<br>
data Vec {a} (A : Set a) : Nat → Set a where<br>
nil : Vec A 0<br>
cons : ∀ {n} → A → Vec A n → Vec A (suc n)<br>
<br>
module _ {a b} {A : Set a} (B : Nat → Set b) where<br>
<br>
fold : ∀ {n} → Vec A n → (∀ {n} → A → Vec A n → B n → B (suc n))
→ B 0 → B n<br>
fold nil c n = n<br>
fold (cons x xs) c n = c x xs (fold xs c n)<br>
<br>
module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where<br>
<br>
zip-with : ∀ {n} → (A → B → C) → Vec A n → Vec B n → Vec C n<br>
zip-with f xs ys = fold P xs step base ys where<br>
<br>
P : Nat → Set _<br>
P n = Vec B n → Vec C n<br>
<br>
step : ∀ {n} → A → Vec A n → P n → P (suc n)<br>
step x xs rec yys = fold (Vec C) yys (λ y ys → cons (f x y)) nil<br>
<br>
base : P 0<br>
base _ = nil<br>
================================================================<br>
<br>
Cheers,<br>
<br>
</tt><br>
<div class="moz-cite-prefix">On 17/02/18 10:37, v0ιd wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAE3YR0U6fq9jJQU7+ynt3cj3GaHh=WyEYY8gdiwnT2yzmVvKMQ@mail.gmail.com">
<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>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>