DataCodata.agda

module DataCodata where

open import Data.Product using (_×_ ; _,_)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)


--------------------------------------------------------------------------------


case : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″}
                   → X ⊎ Y → (X → Z) → (Y → Z)
                   → Z
case (inj₁ x) f g = f x
case (inj₂ y) f g = g y


--------------------------------------------------------------------------------


data List {ℓ} (X : Set ℓ) : Set ℓ
  where
    cons : X → List X → List X
    nil  : List X

it : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′}
              → List X → (X → Y → Y) → Y
              → Y
it (cons x xs) f y = f x (it xs f y)
it nil         f y = y

rec : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′}
               → List X → (X → List X × Y → Y) → Y
               → Y
rec (cons x xs) f y = f x (xs , rec xs f y)
rec nil         f y = y


--------------------------------------------------------------------------------


record Stream {ℓ} (X : Set ℓ) : Set ℓ
  where
    coinductive
    field
      hd : X
      tl : Stream X

open Stream

coit : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′}
                → (Y → X) → (Y → Y) → Y
                → Stream X
hd (coit f g y) = f y
tl (coit f g y) = coit f g (g y)

corec : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′}
                 → (Y → X) → (Y → Stream X ⊎ Y) → Y
                 → Stream X
hd (corec f g y) = f y
tl (corec f g y) with g y
...              | inj₁ xs = xs
...              | inj₂ y′ = corec f g y′


-- NOTE: Fails termination check

-- tl (corec f g y) = case (g y)
--                      (λ xs → xs)
--                      (λ y′ → corec f g y′)


--------------------------------------------------------------------------------

DataCodata.hs

{-# LANGUAGE FlexibleInstances, GADTs, MultiParamTypeClasses, Rank2Types #-}

module DataCodata where


-- Iterator
it :: [a] -> (a -> b -> b) -> b -> b
it (x : xs) f y = f x (it xs f y)
it []       f y = y

-- Recursor
rec :: [a] -> (a -> ([a] , b) -> b) -> b -> b
rec (x : xs) f y = f x (xs , rec xs f y)
rec []       f y = y


-- Streams, in a final encoding
class Stream s a where
  hd :: s a -> a
  tl :: s a -> s a


-- Lists are streams, as long as we don't mind some runtime failures
instance Stream [] a where
  hd (x : xs) = x
  tl (x : xs) = xs


-- Coiterator: declaration
data Coit a b where
  Coit :: (a -> b) -> (a -> a) -> a -> Coit a b

-- Coiterator: definition
instance Stream (Coit a) b where
  hd (Coit f g x) = f x
  tl (Coit f g x) = Coit f g (g x)


-- Corecursor: declaration
data Corec a b where
  Corec :: (a -> b) -> (a -> Either (Corec a b) a) -> a -> Corec a b

-- Corecursor: definition
instance Stream (Corec a) b where
  hd (Corec f g x) = f x
  tl (Corec f g x) = case g x of
                       Left ys  -> ys
                       Right x' -> Corec f g x'


-- Constant stream of ()s: declaration
data Units a where
  Units :: Units a

-- Constant stream of ()s: definition
instance Stream Units () where
  hd Units = ()
  tl Units = Units


-- Constant stream of 1s: declaration
data Ones a where
  Ones :: Ones a

-- Constant stream of 1s: definition
instance Num a => Stream Ones a where
  hd Ones = 1
  tl Ones = Ones

DataCodata.txt

data List X where
  cons : X → List X → List X
  nil  : List X
  
it : List X → (X → Y → Y) → Y → Y
it (cons x xs) f y = f x (it xs f y)
it nil         f y = y

rec : List X → (X → List X × Y → Y) → Y → Y
rec (cons x xs) f y = f x (xs , rec xs f y)
rec nil         f y = y


codata Stream X where
  hd : Stream X → X
  tl : Stream X → Stream X

coit : (Y → X) → (Y → Y) → Y → Stream X
hd (coit f g y) = f y
tl (coit f g y) = coit f g (g y)

corec : (Y → X) → (Y → Stream X + Y) → Y → Stream X
hd (corec f g y) = f y
tl (corec f g y) = case (g y)
                     (λ xs → xs)
                     (λ y′ → corec f g y′)