[Agda] Recursive definitions over lists

[Philip Wadler]

Thanks!

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.


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?

Cheers, -- P

On Tue, 25 Jun 2019 at 05:58, Guillaume Allais <gallais at cs.ru.nl> wrote:

> 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
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190625/2259935b/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190625/2259935b/attachment.ksh>