FreePartiality.agda

open import Data.Container using (Container; Shape; Position)
open import Data.Container.Combinator using (id)
open import Data.Container.FreeMonad using (_⋆C_)
open import Data.Sum using (inj₂)
open import Data.Unit.Base using (tt)
open import Level using (lift; _⊔_)

record M {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  coinductive
  field
    head : A
    tail : B head → M A B
open M

ν : ∀ {ℓ} → Container ℓ → Set ℓ
ν C = M (Shape C) (Position C)

Partiality : ∀ {ℓ} → Set ℓ → Set ℓ
Partiality A = ν (id ⋆C A)

never : ∀ {ℓ} {A : Set ℓ} → Partiality A
head never = inj₂ (lift tt)
tail never = λ x → never