[Agda] On termination checkers

[Andrew Pitts]

> On 12 Jun 2019, at 10:09, david.janin at labri.fr wrote:
> 
> Dear Andrew,
> 
> To your question, what shall be the best sizing for (inductive) lists,  
> experiment seems to show that the answer is none !!!
> 
> I describe below the arguments with examples piled one on top of the other,  the 
> correct code being enclosed. 
> 
> The experiment consists in trying all discussed definitions of sized (inductive)
> list, dropping the pack/unpack aspects that is now irrelevant, and trying to prove
> some expected (easy) list’s properties.
> 
> The possibilities discussed so far  (given in incorrect « piled » Agda code) are:
> ...
> Or this suggests that sized type are bound to be used with co-induction so that
> escape towards infinity is possible.

I don’t think so. The way I see it is as follows. 

Sized types can be useful with inductive data when one has a recursive definition of a function on the data that is semantically well-defined, but which Agda’s termination check can't see as such. Some sized version of the data type (there may be several different ones!) may allow a definition of the recursive function to pass the checker and do the right thing “at infinity”. But especially for functions of several arguments there could be many different ways (or none!) of introducing size information in the arguments and results that does the job at infinity. So in your experiments I would say it’s not so much a question of which of the data declarations (SList1, SList2 or SList3) is better, as to how to introduce sizes in your select/unchanged/append function definitions — and that delicately depends upon their intended meaning — there won’t be one fixed pattern of what to do (and in some cases it may be impossible). 

Here endeth my 2p worth.

Andy