------------------------------------------------------------------------
-- Andreas Abel and Brigitte Pientka,
-- Wellfounded Recursion with Copatterns and Sized Types.
--
-- Journal of Functional Programming, volume 26, 2016
--
-- Agda code for examples
------------------------------------------------------------------------

{-# OPTIONS --postfix-projections #-}

module Colists where

open import Prelude

------------------------------------------------------------------------
-- Section 2.3 Example: Colists
------------------------------------------------------------------------

data F (A X : Set) : Set where
  nil  : 𝟙 → F A X
  cons : A → X → F A X

record CoList (i : Size) (A : Set) : Set where
  coinductive
  field out : ∀{j : Size< i} → F A (CoList j A)
open CoList

fmap₁ : ∀{A B X} → (A → B) → F A X → F B X
fmap₁ f (nil _)    = nil _
fmap₁ f (cons a x) = cons (f a) x

fmap₂ : ∀{A X Y} → (X → Y) → F A X → F A Y
fmap₂ f (nil _)    = nil _
fmap₂ f (cons a x) = cons a (f x)

module Unfold-Simple where

  -- the coiteration principle

  unfold : ∀{i A S} → (S → F A S) → S → CoList i A
  unfold f s .out = fmap₂ (unfold f) (f s)

  -- repeat from unfold

  repeat : ∀{A} → A → CoList ∞ A
  repeat a = unfold {S = 𝟙} (λ _ → cons a _) _

-- repeat directly

repeat : ∀{i A} → A → CoList i A
repeat a .out = cons a (repeat a)

-- precise typing for unfold

unfold : ∀{i A} (S : Size → Set)
  → (∀{i} → S i → ∀{j : Size< i} → F A (S j))
  → S i → CoList i A
unfold S f s .out = fmap₂ (unfold S f) (f s)

-- map via unfold
-- (needs pattern matching lambda as in the paper)

map : ∀{i A B} → (A → B) → CoList i A → CoList i B
map f = unfold (λ i → CoList i _) λ{ s → fmap₁ f (s .out) }