Rename `WeaklyDecidable`?

[jamesmckinna]

In #2330 / #2336 @JacquesCarette objects to the term-of-art WeaklyDecidable (under Relation.Unary and Relation.Binary.Definitions) as the predicate/relation lifting of Maybe to proxy for (the result type of) semi-decidable properties (just =def "definitely true, with a witness"; nothing =def "don't know"), where by contrast with the usual recursion-theoretic terminology, because functions returning a 'WeaklyDecidable' result are by assumption total, we have a slightly sharper meaning/intention than being 'merely' semi-decidable...

So a question arises, as to whether we continue with the (arguably, unsatisfactory) present terminology/naming, or deprecate in favour of something else... in which case what?

I guess I personally could be happy with SemiDecidable, provided we comment appropriately as to the above sharpening of the usual meaning... alternatively such a name could be reserved for (a renaming of) the codata notion of Delay... in which case what do we call "total semi-decidable properties"? (I hope not TotalSemiDecidable! ;-))

[JacquesCarette]

TotalSemiDecidable for the name of the abstract property seems fine. As a root for the naming convention for 'instances', I agree that it is awful.

decYes ? As in 'decide but give me evidence just in the Yes case'? All Agda functions are total, so we don't need to have that knowledge in the function name. decIsYes ?

weakDec is oddly biased and it's not clear in its name. Hmm, squashNo for the current weakDec? forgetNo?

[jamesmckinna]

Reflecting on #2330 / #2336 and #2059 / #2405 , it's hard not to think that the use of Maybe should perhaps itself be deprecated, given that the From-*/from-* idiom provides a dependently-typed version of Maybe, with Data.Unit.Polymorphic.Base.⊤ proxying for nothing...

One thing that is noteworthy about the use of Maybe in the *.*Solver modules (and perhaps elsewhere) is that there is/seems to be no attempt made to leverage do-notation for the Maybe monad in order to streamline its use. Using Maybe might seem defensible on the model of 'emulate haskell where possible', but we seem not to be getting the best of either world-view...?

[JacquesCarette]

I wouldn't quite use 'deprecate' to describe the situation, although I think we agree on the core: we have to opportunity to benefit from dependent types here, and yet by being too Haskell-like, we don't, even when we could (i..e do). Certainly most Maybe-based APIs should be critically revisited with an eye towards more evidency-yielding APIs.

Maybe is not very far away from "boolean blindness" after all.

[jamesmckinna]

'Maybe myopia'?

[TOTBWF]

Agree with @JacquesCarette here; WeaklyDecidable isn't a great alias, and it just complicates the import graph. I would really caution against SemiDecidable; that name is already occupied by a much sharper property (EG: a type P is semidecidable if there is a function f : Nat -> Bool such that P is equivalent to the mere existence of some n with f n = true).

[jamesmckinna]

Thanks Reed.

The irony of not being able to use SemiDecidable (a name taken in 1-lab, but not yet in stdlib, I think?) is that we need a name for the weaker property than the sharp(er) one you offer... ;-) (there's are perhaps separate question about trading between functions f : Nat -> Bool and Decidable predicates on Nat... never mind the weakening of Nat to general A here... and the contrast between Bool and Maybe... that is, why make Σ₁-Decidable depend necessarily on Nat, when it could be generalised... do you need enumerability of Nat for your definition?)

As for the dependency graph, I would still want to insist on it being worthwhile to distinguish Maybe as a type/Set constructor, from WeaklyDecidable as a property of Sets, Preds, Rels... so if you have a better way of achieving that aim, I'm all ears! Perhaps the first step is, indeed, to split off WeaklyDecidable (and Irrelevant) as part of the stdlib API under Relation.Nullary.WeaklyDecidable, and then we can debate each of

• the name
• the API for the concept

Indeed, doing so now could be non-breaking/v2.3 as you indicate on #2624 , and the outcome of the debate could form the basis for a breaking v3.0 proposal if necessary...

[jamesmckinna]

To follow up on my last edit, I imagining something like: say that Q is Σ₁-_ P if:

• P is a polymorphic type constructor (Maybe, Decidable, ...), with a success criterion success : (a : A) → P A (just, yes, ...)
• there is a representing type Enum (enumerable in some way?)
• a representing predicate enum : (e : Enum) → P Enum
• a (weak) equivalence between Q and ∃[ e ] enum e ≡ success e

Then your SemiDecidable would be Σ₁- Decidable for Enum = Nat, and replacing f with an appropriate enum tracking not f n ≡ true, but the corresponding Decidable/yes analog...

... and WeaklyDecidable could be massaged into the form of Σ₁- Maybe ...?

(Or some such... somewhat chaotically brain-storming this morning... the types of things don't seem to be quite right yet)

[TOTBWF]

We actually don't have SemiDecidable yet! The reason why is exactly the one you stated; I haven't found a nice enough story
for generalizing beyond Nat. I suspect that it has something to do with free omega-CPOs, but I haven't spent the time to investigate further.

I do like the idea of re-phrasing in terms of some sort of "weak enumeration"; will ponder for a bit.

[jamesmckinna]

I think I was after having a definition of SemiDecidable on the model of RecursivelyEnumerable (which we also don't have!) as Σ₁- Recursive in descriptive/arithmetic hierarchy terms, but wanting to generalise over Nat, and wondering what properties it actually required for such definitions to be 'good'/well-behaved. Back to Soare or Barwise, I suppose, and then some hard sums... not quite sure where the free omega-CPOs might come in, but interested if/when you figure out the details!