Make some Dec operations more easily accessible?

[masaeedu]

Hello there. I was doing some stuff with decidable equality and ended up needed the following operations:

  imap : ∀ {ℓ} {a b : Set ℓ} → (a → b) → (b → a) → Dec a → Dec b
  imap f _ (yes x) = yes (f x)
  imap _ g (no  x) = no $ x ∘ g

  zip : ∀ {ℓ} {a b : Set ℓ} → Dec a → Dec b → Dec (a × b)
  zip (yes x) (yes y) = yes $ (x , y)
  zip (no  x) _       = no $ λ { (x' , _) → x x' }
  zip _       (no  y) = no $ λ { (_ , y') → y y' }

  _∪_ : ∀ {ℓ} {a b : Set ℓ} → Dec a → Dec b → Dec (a ⊎ b)
  _∪_ (yes a) _ = yes (inj₁ a)
  _∪_ (no  a) b = imap inj₂ ([ ⊥-elim ∘ a , id ]′) b

Does it make any sense to add these to the Relation.Nullary module that Dec is exported from?

[masaeedu]

zip and _∪_ respectively have the following units, but doesn't seem to be much of a use for exporting these given that they're very thin aliases for stuff that's already exported under other names:

  pure : ∀ {ℓ} {a : Set ℓ} → a → Dec a
  pure = yes

  ∅ : Dec ⊥
  ∅ = no ⊥-elim

[gallais]

This is respectively:

• map′
• _×-dec_
• _⊎-dec_

[masaeedu]

Doii, should have looked around more. Thanks

[gallais]

No bother. I myself find it annoying that you have to import 3 or 4 modules to
start working with Dec. I wonder whether we could reorganise this part of the
hierarchy in a backwards-compatible manner that would allow you to import, say
Relation.Decidability and have immediately access to a whole host of functions.

Edit: I have hijacked this issue to discuss such a change.

[JacquesCarette]

I am definitely a big fan of having the "developer's library" be made of tons of small files with carefully crafted minimal dependencies, and a "user's library" with fewer modules that provide 'broad utility' with few imports. Both would be part of the standard library.

[MatthewDaggitt]

Mimic structure of e.g. Relation.Unary by moving Nullary.Product etc. contents into the main module and decidability to Relation.Nullary.Properties module. Put out an RFC before merging.