[Agda] On termination checkers

[Andrew Pitts]

Hello Guillaume.

> On 11 Jun 2019, at 08:53, Guillaume Allais <guillaume.allais at ens-lyon.org> wrote:
> 
> The main difference comes when you try to prove decidable equality
> of sized values (or anything that processes values in lock step).
> Let us consider the case where we compare `t u : PList A i` which
> happen to respectively be `t = pcons a t'` and `u = pcons b u'`.
> 
> If you use `↑ i` as the return index in the `pcons` constructor then
> you learn that `i = ↑ i'` and both `t' u' : Pack (PList A i')`. You
> can keep comparing the subterms.
> 
> Using the `Size< i` approach however, you get that `t' : Pack (PList A j)`
> for some `j` and `u' : Pack (PList A j')` for some a priori distinct `j'`.
> You are now stuck with subterms which have different types and the
> comparison function cannot be homogeneous anymore.

Thanks for that. I see the problem, but I’m not entirely convinced that one couldn’t work around such problems while still using the size-"size-parameterized” approach rather than the “size-indexed” one. In particular...

> This is part of the motivation for Abel, Vezzosi and Winterhalter's
> work on shape irrelevance in https://hal.archives-ouvertes.fr/hal-01596179 <https://hal.archives-ouvertes.fr/hal-01596179>

...thanks for pointing to that. I contemplated their motivating example (monus-diag in section 2) and came up with a simple solution the "size-parameterized” way (hence avoiding the need to contemplate shape irrelevancy, interesting though that might be). See the attached file of agda code if you are interested. 

Anyway, I think my main difficulty with sized types à la Agda is that they introduce some quite non-trivial subtype relations (very un-Agda-ish :-)) and I am finding it hard to understand when Agda thinks one type involving size expressions is a subtype of another such type and when it doesn’t. 

Andy

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190611/321ee98b/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: SizedNat.agda
Type: application/octet-stream
Size: 1997 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190611/321ee98b/attachment.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190611/321ee98b/attachment-0001.html>