open import 1Lab.Prelude

open import Data.Maybe.Base
open import Data.List.Base
open import Data.Nat.Base
open import Data.Dec

module Data.Partial.Base where

private variable
  o o' ℓ : Level
  A B C : Type ℓ

The partiality monad🔗

The partiality monad is an approach to modelling partial computations in constructive type theory — computations which may fail. The meaning of failure depends on the specific computation: for example, it might be non-terminating, or undefined on a given input. The partiality monad abstracts away from these details to arrive at the general notion of partial elements.

A partial element $x$ of a type $A$ consists of a predicate $d:\Omega$ and a function $x:d\to A\text{.}$ We refer to $d$ as the extent of definition of the partial element, since its function is to record precisely where a given element is defined. The function contained within produces an element $x(-):A$ on that extent.

record ↯ {ℓ} (A : Type ℓ) : Type ℓ where
  no-eta-equality
  field
    def : Ω
    elt : ∣ def ∣ → A

We note that, while each element of ↯ stores a proposition — and, therefore, a type — the type $↯A$ of partial $A\text{-elements}$ lives in the same universe level as $A$ itself. This is because of our standing assumption of propositional resizing. Were it not for this assumption, we would additionally need to quantify over a level $\ell$ bounding the size of the extents, generating an $\ell \text{-large}$ type of $\ell \text{-partial}$ elements.

open ↯ public

instance
  Underlying-Part : Underlying (↯ A)
  Underlying-Part = record { ℓ-underlying = lzero ; ⌞_⌟ = λ x → ⌞ x .def ⌟ }

abstract
  ↯-indep : (x : ↯ A) {p q : ⌞ x ⌟} → x .elt p ≡ x .elt q
  ↯-indep x = ap (x .elt) (x .def .is-tr _ _)

Part-pathp
  : {x : ↯ A} {y : ↯ B} (p : A ≡ B) (q : x .def ≡ y .def)
  → PathP (λ i → ∣ q i ∣ → p i) (x .elt) (y .elt)
  → PathP (λ i → ↯ (p i)) x y
Part-pathp {x = x} {y = y} p q r i .def = q i
Part-pathp {x = x} {y = y} p q r i .elt = r i

Partial elements enjoy the following extensionality principle: $x=y$ whenever they are defined on equivalent extents, and they agree whenever defined.

part-ext
  : {x y : ↯ A} (to : ⌞ x ⌟ → ⌞ y ⌟) (of : ⌞ y ⌟ → ⌞ x ⌟)
  → (∀ xd yd → x .elt xd ≡ y .elt yd)
  → x ≡ y
part-ext to from p = Part-pathp refl
  (Ω-ua to from) (funext-dep λ _ → p _ _)

To close the initial definitions, if we have a partial element $x:↯A$ and a total $y:A\text{,}$ then we write $x\downarrow y$ for the relation $x$ is defined and $x(-)=y$:

_↓_ : ↯ A → A → Type _
x ↓ y = Σ[ d ∈ x ] (x .elt d ≡ y)

instance
  Membership-↯ : Membership A (↯ A) _
  Membership-↯ = record { _∈_ = λ x p → p ↓ x }

abstract instance
  H-Level-↯ : ∀ {A : Type ℓ} {n} ⦃ _ : 2 ≤ n ⦄ ⦃ _ : H-Level A n ⦄ → H-Level (↯ A) n
  H-Level-↯ {n = suc (suc n)} ⦃ s≤s (s≤s p) ⦄ =
    hlevel-instance $ Iso→is-hlevel! (2 + n) eqv
    where unquoteDecl eqv = declare-record-iso eqv (quote ↯)

The information ordering🔗

The information ordering on partial elements embodies the idea that $x:↯A$ is a computation valued in $A\text{:}$ If we have two such computations $x,y\text{,}$ there is an emergent notion of one having made more progress than the other — for example, if we were to model them as Turing machines, one might have literally taken more steps than the other.

We write the information ordering as $x⊑y\text{:}$ it holds whenever $x$ is more defined than $y\text{,}$ and they agree on this common extent.

record _⊑_ {ℓ} {A : Type ℓ} (x y : ↯ A) : Type ℓ where
  no-eta-equality
  field
    implies : ⌞ x ⌟ → ⌞ y ⌟
    refines : ∀ xd → y .elt (implies xd) ≡ x .elt xd

open _⊑_ public

abstract instance
  H-Level-⊑ : ∀ {A : Type ℓ} {x y : ↯ A} {n} ⦃ _ : 1 ≤ n ⦄ ⦃ _ : H-Level A (suc n) ⦄ → H-Level (x ⊑ y) n
  H-Level-⊑ {n = suc n} ⦃ s≤s p ⦄ = hlevel-instance $ Iso→is-hlevel! (suc n) eqv
    where unquoteDecl eqv = declare-record-iso eqv (quote _⊑_)

At the bottom element in the information order, we have the computation which never succeeds.

never : ↯ A
never .def = ⊥Ω

Monadic structure🔗

We claimed above that the type of partial elements is a monad: equipped with the information order, it’s actually the free pointed directed-continuous partial order on a set. However, it’s also a monad in the looser sense of supporting do notation.

We can define the necessary components here, without getting out the entire adjoint functor machinery. First, we note that function composition lets us extend $A\to B$ to $↯A\to ↯B\text{:}$

part-map : (A → B) → ↯ A → ↯ B
part-map f x .def = x .def
part-map f x .elt = f ∘ x .elt

Then, we can define the transformation $A\to ↯A\text{,}$ and the “extension” operator part-bind. This latter definition highlights an important feature of $\Omega \text{:}$ it is closed under dependent sums. A type of propositions closed under dependent sums is called a dominance.

always : A → ↯ A
always a .def   = ⊤Ω
always a .elt _ = a

part-bind : ↯ A → (A → ↯ B) → ↯ B
part-bind x f .def .∣_∣   = Σ[ px ∈ x ] (f ʻ x .elt px)
part-bind x f .def .is-tr = hlevel 1
part-bind x f .elt (px , pfx) = f (x .elt px) .elt pfx

We note that we can also lift the operation of function application to the application of partial functions to partial arguments: we get a result whenever they are both defined.

part-ap : ↯ (A → B) → ↯ A → ↯ B
part-ap f x .def .∣_∣      = ⌞ f ⌟ × ⌞ x ⌟
part-ap f x .def .is-tr    = hlevel 1
part-ap f x .elt (pf , px) = f .elt pf (x .elt px)

is-always : {A : Type ℓ} (a : ↯ A) (x : ⌞ a ⌟) → a ≡ always (a .elt x)
is-always a x = part-ext (λ _ → tt) (λ z → x) λ _ _ → ↯-indep a

always-injective : {A : Type ℓ} {x y : A} → always x ≡ always y → x ≡ y
always-injective p = ap₂ unalways p q where
  unalways : (x : ↯ A) → ⌞ x ⌟ → A
  unalways = elt

  q : PathP (λ i → ⌞ p i ⌟) tt tt
  q = is-prop→pathp (λ i → p i .def .is-tr) tt tt

instance
  ↯-Map : Map (eff ↯)
  ↯-Map .Map.map = part-map

  ↯-Idiom : Idiom (eff ↯)
  ↯-Idiom .Idiom.Map-idiom = ↯-Map
  ↯-Idiom .Idiom.pure      = always
  ↯-Idiom .Idiom._<*>_     = part-ap

  ↯-Bind : Bind (eff ↯)
  ↯-Bind .Bind._>>=_      = part-bind
  ↯-Bind .Bind.Idiom-bind = ↯-Idiom

-- This class lets us define syntax sugar for e.g. lifted binary
-- operators which automatically lifts values from the base type
record To-part {ℓ'} (X : Type ℓ') (A : Type ℓ) : Type (ℓ ⊔ ℓ') where
  field to-part : X → ↯ A

instance
  part-to-part : To-part (↯ A) A
  part-to-part = record { to-part = λ x → x }

  pure-to-part : To-part A A
  pure-to-part = record { to-part = always }

What about Maybe?🔗

In functional programming circles, it’s common to define a partial function $A\to B$ to be a total function $A\to \mathrm{Maybe}(B)\text{.}$ The Maybe type is certainly simpler than our ↯: so why not use that?

The answer lies, as it so often does, in constructivism. The functions $f:A\to \mathrm{Maybe}(B)$ are precisely those for which it is decidable whether or not $f(x)$ is defined, for each $x:A\text{.}$ But if we do not accept the law of excluded middle, then using the proper partiality monad gains us actual generality.

We can prove that the type Maybe A is equivalent to the subtype of ↯ A with decidable extent, by writing simple functions back and forth:

↯-Maybe : ∀ {ℓ} → Type ℓ → Type ℓ
↯-Maybe A = Σ[ p ∈ ↯ A ] Dec ⌞ p ⌟

maybe→↯-maybe : Maybe A → ↯-Maybe A
maybe→↯-maybe nothing  = never , auto
maybe→↯-maybe (just x) = always x , auto

↯-maybe→maybe : ↯-Maybe A → Maybe A
↯-maybe→maybe (x , yes x-def) = just (x .elt x-def)
↯-maybe→maybe (x , no ¬x-def) = nothing

maybe→↯→maybe : (x : Maybe A) → ↯-maybe→maybe (maybe→↯-maybe x) ≡ x
maybe→↯→maybe nothing  = refl
maybe→↯→maybe (just x) = refl

↯→maybe→↯ : (x : ↯-Maybe A) → maybe→↯-maybe (↯-maybe→maybe x) ≡ x
↯→maybe→↯ (x , yes a) = Σ-prop-path! $ part-ext (λ _ → a) (λ _ → tt)
  (λ _ _ → ↯-indep x)
↯→maybe→↯ (x , no ¬a) = Σ-prop-path! $ part-ext (λ ()) ¬a λ ()

However, we can not prove that this is a genuine generalisation. That is because constructive type theory is compatible with the law of excluded middle, but if we could internally demonstrate an undecidable proposition, it would contradict the law of excluded middle.