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

[jamesmckinna]

After the recent slew of PRs based on the 'subset-as-family' idiom, I'm happy to row back on my suggestions regarding Level parameterisation/(im)predicativity, and take a fresh(er) look at the current draft.

[jamesmckinna]

Very nice, and I look forward to seeing this land, after appropriate revisions.

[jamesmckinna]

Re: the construction as a partial map classifier.

At the moment, this only provides the 'raw' type constructor, without any additional Setoid-fu to make it a construction fitting into the existing Setoid-based hierarchy of 'sets and functions' as the (concrete) basis for (abstract) algebra.

Fine as far as that goes, as we don't even have machinery (yet) for partial functions, besides my speculative #2816 , so I'm interested in where this PR might go downstream in terms of fleshing out that, or any alternative, vision for such things.

[JacquesCarette]

So it looks like this one might be ready after all? @jamesmckinna what is outstanding?

[jamesmckinna]

So it looks like this one might be ready after all? @jamesmckinna what is outstanding?

I'll need to come back to this and think! Plus get more sleep than I'm currently managing to achieve.

UPDATED: needs CHANGELOG at a minimum. Other stuff I'm still thinking about, but I would double down on makin g never and always Level-polymorphic... the previous suggestions weren't applied! UPDATED: now done.

@e-mniang are you still interested in working on this, and/or able to do so? If not, I think that between @JacquesCarette and myself we can try to merge this in soon. In any case, converting back from DRAFT with this in mind...

I've started looking at this again, making changes previously suggested but not acted upon, and so my former review shouldn't be considered blocking any more.

[jamesmckinna]

@JacquesCarette I think this now is a minimal commit-able bunch of code, but lacking @TOTBWF 's gloss/commentary. Will add later, unless Reed, do you want to?

[jamesmckinna]

Question for @JacquesCarette and @TOTBWF :

• the difference between this contribution for stdlib and that for 1lab is that Dom isn't required to be a Prop/subsingleton/subobject of 1, so should that in fact be part of the definition?
• wrt this, never corresponds to the subsingleton which is actually empty; always to the definitely inhabited singleton, as the 'two' extremal examples...
• ... but what about

  weird : ↯ A _
  weird {A = A} = record { Dom = A ; dom = id }

On its face, this typechecks correctly (at level a if A : Set a), but what on earth does it correspond to, considered as a 'partial' inhabitant of A. If A is already a subsingleton (I'd be tempted to qualify the Dom field declaration with an irrelevance modality, but as discussed elsewhere, this may not be the moment to open that can of worms... cf. agda/agda#8557), then weird, although weird, is more-or-less 'obviously equivalent' to always. But without any such stipulation... what exactly do we have here?

Proposal: we park this PR unmerged, until such time as we resolve the irrelevance/Prop issue, or else ... well I'm not quite sure!?

Please chime in on this, otherwise I'm not sure that this should go through even as it now is.

(Reading back over my earliest comment, I did ask about what might be the consequences of dropping the Prop/subsingleton restriction... sorry it's taken so long to return to my first thought!)

[TOTBWF]

If you remove the subsingleton condition then you get a multi-map classifier instead of a partial map classifier.

A → ↯ B 
≅ A → Σ (Dom : Set) (Dom → B) -- by defn
≅ A → (B → Set) -- Fibre-family equivalence[1]

After some thought, I think this is actually what you'd want in the stdlib. If you are working with setoids, then the right notion of subsingleton is ∀ x y → x ≈ y. This has some consequences for the theory of partial functions: the right notion of partiality is that the domain of definition is a setoidal subsingleton. This means things like the codiscrete setoid will have an underlying multimap, not an underlying partial map.

As for weird, this is actually a very handy trick. One way of viewing
↯ A is that it's a value of A guarded behind some assumptions that we will discharge later. From this perspective, weird lets you add an assumption that you will need to discharge later. This is very useful when programming in the partiality/multimap monad; it's basically a proof-relevant, witness providing form of guard :: Bool -> m () or assert.

I would definitely not make Dom a Prop or irrelevant though! Both will be rather ill-behaved when you want to use weird (or it's subsingleton version where the domain of definition is Σ (x : A) (∀ y → x = y)) to cook up things like termination witnesses. Moreover, neither Prop nor irrelevance supports unique choice[^2] which will cause problems when you try to take directed joins.

[^1] This step may or may not need univalence depending on the notion of isomorphism/equivalence of types you use.

[^2] Modulo the bug where you get global choice lol

[JacquesCarette]

I believe the "global choice" bug has been fixed by Jesper in current development Agda, and ought to be in 2.9.

[jamesmckinna]

On the basis of @TOTBWF 's comments, I'd be happy to merge now.