[Agda] On termination checkers

[Andrew Pitts]

> 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))
> -----------------------------------------------------------------------