[Agda] Recursive definitions over lists

[Philip Wadler]

Consider the following code.

\begin{code}
module Tree where

  open import Data.List using (List; []; _∷_; map)
  open import Data.List.All using (All; []; _∷_)

  data Tree (A : Set) : Set where
    node : List (Tree A) → Tree A

  mapTree : ∀ {A B : Set} → (A → B) → Tree A → Tree B
  mapTree f (node ts)  =  node (map (mapTree f) ts)

  mapTree′ : ∀ {A B : Set} → (A → B) → Tree A → Tree B
  mapForest′ : ∀ {A B : Set} → (A → B) → List (Tree A) → List (Tree B)

  mapTree′ f (node ts)   =  node (mapForest′ f ts)
  mapForest′ f []        =  []
  mapForest′ f (t ∷ ts)  =  mapTree′ f t ∷ mapForest′ f ts

  data AllTree {A : Set} (P : A → Set) : Tree A → Set where
    node : ∀ {ts : List (Tree A)}
      → All (AllTree P) ts
        -------------------
      → AllTree P (node ts)
\end{code}

Agda complains that the first definition of mapTree may not terminate.

    Termination checking failed for the following functions:
      mapTree
    Problematic calls:
      mapTree f
        (at /Users/wadler/Desktop/Tree.lagda:11,38-45)

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.

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?

I'm surprised to note that Agda does not make a similar complaint about the
definition of AllTree. Why not?

Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190624/dd062560/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Tree.lagda
Type: application/octet-stream
Size: 1661 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190624/dd062560/attachment.obj>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190624/dd062560/attachment.ksh>