[add] partial elements in Effect.Monad.Partial module

[e-mniang]

This PR introduces the ↯ type for partial elements along with its associated functions for binding, mapping, and applying.

Partial computations — such as non-terminating functions or computations undefined on some input — are represented by a domain of definition and an associated function. The type ↯ A ℓ encapsulates such partial values over a type A by:

record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where
  field
    Dom : Set ℓ'
    elt : Dom → A

Basic constructors:

    never : nowhere-defined partial element

    always : total value lifted into a partial one

Functions:

bind↯ : monadic bind

map↯ : functorial map

ap↯ : applicative operator

---

Source: https://1lab.dev/Data.Partial.Base.html#1132 and @TOTBWF

[MatthewDaggitt]

Hi @e-mniang, thanks for the contribution! I've requested reviews from people who may be more capable of assessing this than me. However, for starters please could you make sure that your proposed new file has the same formatting as all the other files in the standard library?

[e-mniang]

Hi! Thanks for your comment.
I made some changes and I hope the file is now in the correct format. :)

[jamesmckinna]

@MatthewDaggitt requested my review, but ahead of any such, my first thought would be: why is the Level of the domain universally quantified in the definition, and not existentially?:

record ↯ {a} (A : Set a) : Set ω where
  field
    ℓ : Level
    Dom : Set ℓ
    elt : Dom → A

I realise that Setω is not everyone's cup of tea, but it strikes me that such a definition is closer in spirit to saying "there is some domain of definition" which I (perhaps mistakenly) presume to be part of the data for 'partiality'.

An alternative might be to define 'partial function from A to B', in which we could constrain the level of the domain to be bounded by that of A (actually: could we do that here, simply by taking a as the level of Dom?) and then the type of 'partial elements of A' would be given by 'partial function from Data.Unit.Polymorphic.⊤ to A'?

I'll try to look at the 1lab to see what's going on there (oh, some quite delicate things under the hood about a small type of propositions... and the level that such a thing should live at. Hmmm). And perhaps also go back to Eugenio Moggi's PhD thesis, and Scott's "Identity and Existence in Intuitionistic Logic" (Springer LNM 753) for a refresher course...

Also: Codata.Sized.Delay and friends?

[gallais]

Also: Codata.Sized.Delay and friends?

We indeed have e.g. https://agda.github.io/agda-stdlib/v2.2/Effect.Monad.Partiality.html

[jamesmckinna]

Also: Codata.Sized.Delay and friends?

We indeed have e.g. https://agda.github.io/agda-stdlib/v2.2/Effect.Monad.Partiality.html

So... that leaves some tricky design choices as to how to proceed with this PR, if we think it is worth doing so:

• for example, can we show that Effect.Monad.Partiality gives rise to an instance of the structure you define above? Eg. consider the subset of A ⊥ with domain defined by _⇓ (via Data.Refinement or a vanilla Σ-type...), with inclusion given by the obvious thing...
• can you go in the opposite direction (that seems harder?)
• what, if any, are the consequences of (giving up on the details of) the 1lab type Ω of small propositions etc. in your definition?
• what properties of 'partial' elements/functions in 1lab are missing from the analysis/properties of the _⊥ monad?

So... overall my conclusion (for the time being, at least) is that this PR probably shouldn't proceed, unless there are compelling answers to the above questions?

[TOTBWF]

Delay monads like the one in Effect.Monad.Partiality require some degree of countable choice to be equivalent to the partiality monad here: I think "Quotienting the delay monad by weak bisimilarity" by Chapman et al. has the details. The problem is that delay is too intentional: two things that eventually arrive at the same value might take different numbers of steps. IIRC you still get a monad on the category of setoids if you pick the right equivalence relation, but it's quite delicate, and I don't recall if it actually classifies partial maps.

As for impredicativity, this isn't essential aside from the usual caveats about predicative order theory: see Tom de Jong's thesis for more.

Finally, we could prove the monad laws, though this would require some setoid-fu that quotients away the choice of witnesses of definedness.

[TOTBWF]

Also, I forgot to mention that modulo proof-relevance, this is the free pointed DCPO, whereas delay-like monads are aiming to be the free omega-CPO.

[JacquesCarette]

That level of 'documentation' would be worth putting in the PR, including adding some to the current Partiality monad.

[jamesmckinna]

@TOTBWF wrote:

Also, I forgot to mention that modulo proof-relevance, this is the free pointed DCPO, whereas delay-like monads are aiming to be the free omega-CPO.

Thanks Reed for this. Does this (ie. 'free pointed DCPO') mean that only decidable domains of partial definitions are being considered (because we can distinguish the point?), or is that a misunderstanding based on stdlib (erroneous?) use of Maybe for capturing pointedness?

Also: a propos free-ness (and #1962 #2539 etc. for @JacquesCarette 's shopping list of examples with which to explore candidate designs), are we going to add the relevant universal properties, suitably phrased, at some point downstream... ?