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 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
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.