[Agda] Recursive definitions over lists

[Guillaume Allais]

Hi Phil,

First of all the code-free answer: AllTree is accepted because Agda recorded
internally that `All`'s first argument was only ever used in a strictly
positive manner. It is therefore legal to take the fixpoint of that definition.

Regarding the definition of mapTree, the problem is the level of indirection
introduced by `map`: it is not obvious for Agda that the partially applied
recursive call `mapTree f` will only ever be used on subterms.
As you have observed, inlining `map` is a possible solution to remove this
level of indirection. Another one is to start using sized types so that the
notion of being a subterm becomes a type-level one.

Cf. this recent discussion on the mailing list:
https://lists.chalmers.se/pipermail/agda/2019/011209.html

and in particular this message with code for a similar sized inductive type:
https://lists.chalmers.se/pipermail/agda/2019/011212.html

Cheers,
--
gallais

On 24/06/2019 22:05, Philip Wadler wrote:
> 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/
> 
> 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>