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