<div dir="ltr"><div><div dir="auto">Thanks!</div></div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">AllTree is accepted because Agda recorded<br>internally that `All`'s first argument was only ever used in a strictly<br>positive manner. It is therefore legal to take the fixpoint of that definition.</blockquote><div> </div><div>Can you say more about how this works, or where I can read up on it? Why is All strictly positive but map is not?</div><div><br></div><div>Cheers, -- P</div></div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 25 Jun 2019 at 05:58, Guillaume Allais <<a href="mailto:gallais@cs.ru.nl" target="_blank">gallais@cs.ru.nl</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Phil,<br>
<br>
First of all the code-free answer: AllTree is accepted because Agda recorded<br>
internally that `All`'s first argument was only ever used in a strictly<br>
positive manner. It is therefore legal to take the fixpoint of that definition.<br>
<br>
Regarding the definition of mapTree, the problem is the level of indirection<br>
introduced by `map`: it is not obvious for Agda that the partially applied<br>
recursive call `mapTree f` will only ever be used on subterms.<br>
As you have observed, inlining `map` is a possible solution to remove this<br>
level of indirection. Another one is to start using sized types so that the<br>
notion of being a subterm becomes a type-level one.<br>
<br>
Cf. this recent discussion on the mailing list:<br>
<a href="https://lists.chalmers.se/pipermail/agda/2019/011209.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/pipermail/agda/2019/011209.html</a><br>
<br>
and in particular this message with code for a similar sized inductive type:<br>
<a href="https://lists.chalmers.se/pipermail/agda/2019/011212.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/pipermail/agda/2019/011212.html</a><br>
<br>
Cheers,<br>
--<br>
gallais<br>
<br>
On 24/06/2019 22:05, Philip Wadler wrote:<br>
> Consider the following code.<br>
> <br>
> \begin{code}<br>
> module Tree where<br>
> <br>
>   open import Data.List using (List; []; _∷_; map)<br>
>   open import Data.List.All using (All; []; _∷_)<br>
> <br>
>   data Tree (A : Set) : Set where<br>
>     node : List (Tree A) → Tree A<br>
> <br>
>   mapTree : ∀ {A B : Set} → (A → B) → Tree A → Tree B<br>
>   mapTree f (node ts)  =  node (map (mapTree f) ts)<br>
> <br>
>   mapTree′ : ∀ {A B : Set} → (A → B) → Tree A → Tree B<br>
>   mapForest′ : ∀ {A B : Set} → (A → B) → List (Tree A) → List (Tree B)<br>
> <br>
>   mapTree′ f (node ts)   =  node (mapForest′ f ts)<br>
>   mapForest′ f []        =  []<br>
>   mapForest′ f (t ∷ ts)  =  mapTree′ f t ∷ mapForest′ f ts<br>
> <br>
>   data AllTree {A : Set} (P : A → Set) : Tree A → Set where<br>
>     node : ∀ {ts : List (Tree A)}<br>
>       → All (AllTree P) ts<br>
>         -------------------<br>
>       → AllTree P (node ts)<br>
> \end{code}<br>
> <br>
> Agda complains that the first definition of mapTree may not terminate.<br>
> <br>
>     Termination checking failed for the following functions:<br>
>       mapTree<br>
>     Problematic calls:<br>
>       mapTree f<br>
>         (at /Users/wadler/Desktop/Tree.lagda:11,38-45)<br>
> <br>
> I guess this is because it is not quite clever enough to figure out that in<br>
> the definition of (mapTree (node ts)) that the recursive invocation<br>
> (mapTree f) is in fact always applied to a substructure of ts.<br>
> <br>
> One way to get Agda to accept the definition is to rewrite it as two<br>
> mutually recursive functions, one of which expands the definition of map.<br>
> Is this the recommend way to solve the problem, or is there a better<br>
> alternative?<br>
> <br>
> I'm surprised to note that Agda does not make a similar complaint about the<br>
> definition of AllTree. Why not?<br>
> <br>
> Cheers, -- P<br>
> <br>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
> .   /\ School of Informatics, University of Edinburgh<br>
> .  /  \ and Senior Research Fellow, IOHK<br>
> . <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a><br>
> <br>
> <br>
> The University of Edinburgh is a charitable body, registered in<br>
> Scotland, with registration number SC005336.<br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
<br>
</blockquote></div></div>