Free.agda

open import Coinduction using (∞; ♯_)
open import Data.Product using (_×_)
open import Data.Sum using (_⊎_; inj₁)
open import Data.Unit.Base using (⊤; tt)
open import Data.Empty using (⊥)
open import Level using (suc; _⊔_; zero)

data F {α} : Set (suc α) where
  K   : Set α → F
  _+_ : F {α} → F {α} → F
  _*_ : F {α} → F {α} → F
  rec : F

⟦_⟧ : ∀ {α}(f : F {α}) → Set α → Set α
⟦ K B    ⟧ A = B
⟦ a + b  ⟧ A = ⟦ a ⟧ A ⊎ ⟦ b ⟧ A
⟦ a * b  ⟧ A = ⟦ a ⟧ A × ⟦ b ⟧ A
⟦ rec    ⟧ A = A

data Free {α} (f : F {α}) (A : Set α) : Set α where
  pure : A → Free f A
  free : ⟦ f ⟧ (∞ (Free f A)) → Free f A

Partiality : ∀ {α} → Set α → Set α
Partiality = Free rec

never : ∀ {α} {A : Set α} → Partiality A
never = free (♯ never)

MaybeF : F
MaybeF = K ⊤ + rec

terminate : ∀ {A : Set} → Free MaybeF A
terminate = free (inj₁ tt)

onlyPure : ∀ {A : Set} → A → Free (K ⊥) A
onlyPure = pure