Partial Function

A partial function $f:A\rightharpoonup B$ is a function that may not be defined on all inputs.

In set theory this is simply a relation $R_f\subseteq A\times B$ that is left unique:

• $\forall a:A;b_1,b_2:B.(a,b_1),(a,b_2)\in R_f⟹b_1=b_2$.

In type theory this can be represented by an total function to a maybe type, however it is more computationally accurate to use a partiality monad or the delay monad to represent partial computation internally, which expresses non-computability more accuracy. Note that using Maybe fails for non-definable terms such as Godel encoded terms.