[Agda] On termination checkers

[david.janin at labri.fr]

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.

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

Now, I would be the compiler, I would do nothing else but annotating the Plist data type constructor as above with such a size information…
Constructor pnil can also be typed ∀ {i} → PList A  i is fine as well, which I would rather do as a compiler… no need to increase any size here…

What strikes me is that, in the code above,  we say nothing about Pack and unpack… leaving the nevertheless quite smart compiler checking that everything is fine… and even guessing some size constraints in pappend… which can be put to ∞ in both cases as Guillaume showed me.

Is there any hope Adga termination checker can automatically do that for me one day :-)

david


> Le 10 juin 2019 à 14:52, Nils Anders Danielsson <nad at cse.gu.se> a écrit :
> 
> On 10/06/2019 12.41, david.janin at labri.fr wrote:
>> Still, how can I cope with it ? Any suggestion much welcome,
> 
> One option might be to use sized types, but this could lead to other
> complications.
> 
> -- 
> /NAD