search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
561 stars 234 forks source link

Rename `WeaklyDecidable`? #2404

Open jamesmckinna opened 3 weeks ago

jamesmckinna commented 3 weeks ago

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 commented 3 weeks ago

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 commented 3 weeks ago

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 commented 3 weeks ago

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 commented 3 weeks ago

'Maybe myopia'?