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 of a type consists of a predicate and a function We refer to 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 on that extent.

record β†― {β„“} (A : Type β„“) : Type β„“ where
  no-eta-equality
  field
    def : Ξ©
    elt : ∣ def ∣ β†’ A
\ Warning

This notion of partial element is not to be confused with the partial elements which feature in the syntax of cubical type theory!

We note that, while each element of β†― stores a proposition β€” and, therefore, a type β€” the type of partial lives in the same universe level as 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 bounding the size of the extents, generating an type of 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: 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 and a total then we write for the relation is defined and :

_↓_ : β†― 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 is a computation valued in If we have two such computations 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 it holds whenever is more defined than 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 to 

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 and the β€œextension” operator part-bind. This latter definition highlights an important feature of 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)

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

What about Maybe?πŸ”—

In functional programming circles, it’s common to define a partial function to be a total function 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 are precisely those for which it is decidable whether or not is defined, for each 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.