[Agda] On termination checkers

[Guillaume Allais]

Hi Andrew,

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.

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

Cheers,
gallais


On 10/06/2019 15:06, Andrew Pitts wrote:
> 
> 
>> On 10 Jun 2019, at 14:11, david.janin at labri.fr wrote:
>>
>> Indeed, with sized types. 
>>
>> For the record, Guillaume Allais suggested this to me. 
>> His solution is (I think) worth being posted for newbies as I am for it is a fairly simple example of sized type usage with simple inductive data type.
> 
> I have been working quite a lot recently with inductive definitions involving sized types and when I started I could find rather few examples to help me (compared with the number of examples of using sized types with coinductive definitions). One thing I have learnt by trial and error is to try to make sizes parameters rather than indices in data definitions (avoiding mentioning ↑ explicitly as much as possible).
> 
> So I would write your example as
> 
> ——————————————————————————————
> open import Agda.Builtin.Size
> 
> data Pack (A : Set) : Set where
>   pack : A -> Pack  A
> 
> unpack : ∀ {A} -> Pack A -> A
> unpack (pack a) = a
> 
> data PList (A : Set)(i : Size) : Set where
>  pnil  : PList A i 
>  pcons : ∀{j : Size< i} → A -> Pack (PList A j) -> PList A i
> 
> pappend : ∀ {A i} -> PList A i -> PList A _ -> PList A _
> pappend pnil         l = l
> pappend (pcons a pp) l = pcons a (pack (pappend (unpack pp) l))
> ——————————————————————————————
> 
> although I doubt that in this case it make that much difference.
> 
> Perhaps an expert can comment on the pros and cons.
> 
> Andy
> 
> 
>> -----------------------------------------------------------------------
>> open import Size
>>
>> data Pack (A : Set) : Set where
>> pack : A -> Pack  A
>>
>> unpack : ∀ {A} -> Pack A -> A
>> unpack (pack a) = a
>>
>> data PList (A : Set) : Size → Set where
>>  pnil  : ∀ {i} → PList A (↑ i) 
>>  pcons : ∀ {i} → A -> Pack (PList A i) -> PList A (↑ i)
>>
>> pappend : ∀ {A i} -> PList A i -> PList A _ -> PList A _
>> pappend pnil         l = l
>> pappend (pcons a pp) l = pcons a (pack (pappend (unpack pp) l))
>> -----------------------------------------------------------------------
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>