<div dir="ltr"><div>Consider the following code.<br><br>\begin{code}<br><font face="courier new, monospace">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)</font><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 the definition of (mapTree (node ts)) that the recursive invocation (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 mutually recursive functions, one of which expands the definition of map. Is this the recommend way to solve the problem, or is there a better alternative?<br><br>I'm surprised to note that Agda does not make a similar complaint about the definition of AllTree. Why not?<br><br>Cheers, -- P<br></div><div><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr"><br></div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div></div></div>