[Agda] Sized Types: Run-length Encoding Example

[Craig McLaughlin]

Hi all,

I am experimenting with sized types, copattern matching and (co)recursive
definitions. I am trying to define a simple run-length encoding example 
from a
paper by Di Gianantonio and Miculan [1] whose pseudo-code I reproduce below
(the input Stream is an infinite sequence of 0s and 1s):

z :     Stream   ->  Stream
z   (0 :: s)      = 0 :: z(s)
z   (x :: 0 :: s) = x :: 0 :: z(s)
z   (x :: 1 :: s) = x :: z(s),     if x >= 9
z   (x :: 1 :: s) = z(x + 1 :: s), otherwise

My translation into Agda (v2.5.4/stdlib v0.17) is pretty naive and I am
struggling to identify the correct size measure on the definition such that
Agda sees that is terminating. My definition falls down in two places 
which I
describe after presenting the code:

module runlength where

open import Codata.Stream
open import Codata.Thunk
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary
open import Size

mutual
   rlen : ∀ {i} → Stream ℕ (↑ i) → Stream ℕ i
   rlen (zero ∷ xs) = zero ∷ λ where .force → rlen (xs .force)
   rlen (x ∷ xs) = rlen' x (xs .force)

   rlen' : ∀ {i} → ℕ → Stream ℕ i → Stream ℕ i
   rlen' x (zero ∷ xs) =
     x ∷ λ where .force → zero ∷ λ where .force → rlen (xs .force)
   rlen' x (suc zero ∷ xs) with x ≥? 9
   rlen' x (suc zero ∷ xs) | yes p = {!!}
--    x ∷ λ where .force → rlen (xs .force) -- size constraints error
   rlen' x (suc zero ∷ xs) | no ¬p = {!!}
     -- rlen (suc (suc zero) ∷ xs) -- "otherwise" case
   rlen' x (suc (suc y) ∷ xs) = {!!} -- "otherwise" case

---
I believe, the "otherwise" case is the thorniest issue and I haven't seen
anything in the literature on sized types which suggests a solution 
(pointers
much appreciated). Additionally, the "consumption" case for x >= 9 also 
seems
to be problematic since I do not know I can perform another observation 
on xs;
mandated by the size constraint (\up i) in the type of rlen. Is there some
trick to help Agda along?

FWIW, I thought perhaps the stream processor example of Ghani, Hancock, and
Pattinson [2] presented by Abel and Pientka [3] is close to what I'd 
need for
this example but I run into the same issue with the "otherwise" case when
trying to use the mixed datatype defined by SPmu and SPnu.

----
References:

[1] Di Gianantonio P., Miculan M. (2003) A Unifying Approach to 
Recursive and
Co-recursive Definitions. In: Geuvers H., Wiedijk F. (eds) Types for Proofs
and Programs. TYPES 2002. Lecture Notes in Computer Science, vol
2646. Springer, Berlin, Heidelberg

[2] Ghani, Neil, Hancock, Peter, & Pattinson, Dirk. (2009). 
Representations of
stream processors using nested fixed points. Logical Meth. in Comput. Sci.,
5(3:9).

[3] Andreas Abel and Brigitte Pientka (2016). Well-founded recursion with
copatterns and sized types. Journal of Functional Programming, 26, E2.

-- 
Regards,
Craig
http://homepages.inf.ed.ac.uk/s1544843/


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.