[Agda] Sized Types: Run-length Encoding Example

[Jannis Limperg]

Hej Craig,

z is a mixed recursive-corecursive function, meaning that some of its
recursive calls are justified by a termination argument (x gets closer
to 9) and some by a productivity argument (all other cases). There are
two ways to deal with such functions:


A. Elementary Solution

Split the implementation into two functions:

1. a recursive function which generates the first element of the output
stream;
2. a corecursive function which calls the function from (1) infinitely
often and conses the results.


B. Library Solution

For my B.Sc., I developed a library to deal with mixed
recursive-corecursive functions [1]. It defines a fixpoint combinator
that captures the essense of mixed recursion: You can either recurse by
decreasing a well-founded relation, or corecurse 'under a constructor'.
This allows an implementation that looks more or less like the pseudocode.

Unfortunately, the library requires that you encode your data types as
greatest fixed points of container functors, so it comes with
considerable syntactic baggage. However, you could specialise the
fixpoint combinator to streams (or whatever type interests you) to get
rid of the incidental complexity. The library is documented only in my
thesis (available in the repo), but I'll be happy to answer questions if
you want to use it.

Attached is an Agda file with implementations of both solutions.

[1] https://github.com/JLimperg/well-founded-corecursion

Cheers,
Jannis
-------------- next part --------------
module runlength where

open import Data.Bool using (Bool ; true ; false)
open import Data.List as List using (List ; [] ; _∷_)
open import Data.Nat using
  (ℕ ; zero ; suc ; _≟_ ; _∸_ ; _<_ ; _<?_ ; _≤_ ; z≤n ; s≤s)
open import Data.Nat.Properties using (≤-refl)
open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
open import Data.Unit using (⊤)
open import Level using (Level) renaming (zero to lzero)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Relation.Nullary using (Dec ; yes ; no)
open import Size using (Size ; Size<_ ; ∞ ; ↑_)


module Elementary where

  -- I didn't get this approach to work with the standard library's stream type.
  -- Apparently the termination checker is a bit fickle when it comes to
  -- productivity arguments that don't use sizes.
  record Stream (A : Set) : Set where
    coinductive
    field
      head : A
      tail : Stream A

  open Stream


  data Bit : Set where
    zero one : Bit


  -- This implementation is a bit convoluted because I wanted to recurse
  -- structurally over `fuel`, counting down from 9 to 0. Alternatively,
  -- we could use well-founded recursion like in the other solution.
  firstDigit′ : ℕ → ℕ → Stream Bit → ℕ × Stream Bit
  firstDigit′ maxFuel fuel       xs with head xs
  firstDigit′ maxFuel fuel       xs | zero with fuel ≟ maxFuel
  ... | yes _ = zero , tail xs
  ... | no _ = maxFuel ∸ fuel , xs
  firstDigit′ maxFuel zero       xs | one = maxFuel , xs
  firstDigit′ maxFuel (suc fuel) xs | one = firstDigit′ maxFuel fuel (tail xs)


  firstDigit : Stream Bit → ℕ × Stream Bit
  firstDigit = firstDigit′ 9 9


  rlen : Stream Bit → Stream ℕ
  rlen xs
    = let d , xs′ = firstDigit xs in
      λ { .head → d ; .tail → rlen xs′ }


  ones : Stream Bit
  ones = λ { .head → one ; .tail → ones }


  take : ∀ {A} → ℕ → Stream A → List A
  take zero xs = []
  take (suc n) xs = head xs ∷ take n (tail xs)


  test : take 3 (rlen ones) ≡ 9 ∷ 9 ∷ 9 ∷ []
  test = refl


module CoWf where

  open import Coinduction.WellFounded using
    (Container ; _▷_ ; ⟦_⟧ ; M ; inf ; cofixWf)
  open import Induction.Nat using (<-wellFounded)
  open import Induction.WellFounded using
    (WellFounded ; module Inverse-image)


  -- The stream container
  StreamC : Set → Container lzero lzero
  StreamC A = A ▷ λ _ → ⊤


  -- Streams are greatest fixed points of the stream container functor.
  Stream : Set → Size → Set
  Stream A = M (StreamC A)


  -- The unfolding of a stream (i.e. a pair `(head , tail)`).
  StreamU : Set → Size → Set
  StreamU A s = ⟦ StreamC A ⟧ (Stream A s)


  head : ∀ {s} {t : Size< s} {A} → Stream A s → A
  head xs = proj₁ (inf xs)


  tail : ∀ {s A} → Stream A s → {t : Size< s} → Stream A t
  tail xs = proj₂ (inf xs) _


  cons′ : ∀ {s A} → A → Stream A s → StreamU A s
  cons′ x xs = x , λ _ → xs


  cons : ∀ {s A} → A → Stream A s → Stream A (↑ s)
  cons x xs .inf = cons′ x xs


  _<<_ : Rel (Stream ℕ ∞) lzero
  xs << ys = 9 ∸ head xs < 9 ∸ head ys


  <<-wf : WellFounded _<<_
  <<-wf = Inverse-image.wellFounded (λ xs → 9 ∸ head xs) <-wellFounded


  ∸-<-suc : ∀ {n m} → n < m → m ∸ suc n < m ∸ n
  ∸-<-suc {n} {zero} ()
  ∸-<-suc {zero} {suc m} (s≤s n<m) = s≤s ≤-refl
  ∸-<-suc {suc n} {suc m} (s≤s n<m) = ∸-<-suc n<m


  rlenF : ∀ {s} (xs : Stream ℕ ∞)
    → (Stream ℕ ∞ → Stream ℕ s)
    → ((ys : Stream ℕ ∞) → ys << xs → StreamU ℕ s)
    → StreamU ℕ s
  rlenF xs corec wfrec with head xs
  rlenF xs corec wfrec | zero
    = cons′ zero (corec (tail xs))
  rlenF xs corec wfrec | x@(suc _) with head (tail xs)
  rlenF xs corec wfrec | x@(suc _) | zero
    = cons′ x (cons zero (corec (tail (tail xs))))
  rlenF xs corec wfrec | x@(suc _) | y@(suc _) with x <? 9
  rlenF xs corec wfrec | x@(suc _) | y@(suc _) | no _
    = cons′ x (corec (tail xs))
  rlenF xs corec wfrec | x@(suc _) | y@(suc _) | yes x<9
    = wfrec (cons (suc x) (tail (tail xs))) (∸-<-suc x<9)


  rlen : ∀ {s} → Stream ℕ ∞ → Stream ℕ s
  rlen = cofixWf <<-wf rlenF


  ones : ∀ {s} → Stream ℕ s
  ones .inf = 1 , λ _ → ones


  take : ∀ {A} → ℕ → Stream A ∞ → List A
  take zero xs = []
  take (suc n) xs = head xs ∷ take n (tail xs)


  test : take 3 (rlen ones) ≡ 9 ∷ 9 ∷ 9 ∷ []
  test = refl
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190224/2e96f405/attachment.sig>