module Data.Partial.Base where

# 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:Ξ©$
and a function
$x:dβA.$
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

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
$β―A$
of partial
$A-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
$β$
bounding the size of the extents, generating an
$β-large$
type of
$β-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,$
then we write
$xβ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:$
If we have two such computations
$x,y,$
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:$
it holds whenever
$x$
is *more defined than*
$y,$
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βB$ to $β―Aββ―B:$

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ββ―A,$
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*
$AβB$
to be a total function
$AβMaybe(B).$
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βMaybe(B)$
are precisely those for which it is decidable whether or not
$f(x)$
is defined, for each
$x:A.$
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.