search

agda / agda-stdlib

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

Commutative semiring of decidable types #1404

Open conal opened 3 years ago

conal commented 3 years ago

For a project I’m working on, I needed something like a commutative semiring of decidable types. I defined the following existential wrapper to get the homogeneity required by the algebraic structures and bundles:

record Decides : Set (suc ℓ) where
  constructor decides
  field
    {prop} : Set ℓ
    dec : Dec prop

It was fairly easy from there to define structures and bundles up through commutative semirings.

Is this functionality already in agda-stdlib? A quick search for “IsMonoid” didn’t turn up anything obvious.

If this functionality isn’t already in agda-stdlib and if it sounds appealing to others, I’d be happy to package it in a PR, welcoming suggestions for its improvement in the process.

Comments?

MatthewDaggitt commented 3 years ago

Hi Conal, (Typing on my phone so forgive the lack of unicode!)

Assuming that I've understood what your trying to do correctly, I don't believe that functionality currently exists in the standard library. If it did then it would under 'Algebra.Construct'...

If we were going to add it, I'd be tempted to generalise this to the lifting of any algebraic structure with operators that preserve a given predicate P (Dec in your case) to an algebraic structure over the dependant pair of the original element + the instance of P.

Not only would that be more general but then we could then use the \Sigma type rather than defining Decides. You could of course define Decides in terms of the \Sigma and with a little bit of renaming recover most of the behaviour of your custom record type.

Now that I think about it, that'd actually be useful in some of my own code! Cheers, Matthew

On Fri, 22 Jan 2021, 08:29 Conal Elliott, notifications@github.com wrote:

For a project I’m working on, I needed something like a commutative semiring of decidable types. I defined the following existential wrapper to get the homogeneity required by the algebraic structures and bundles:

record Decides : Set (suc ℓ) where

constructor decides

field

{prop} : Set ℓ

dec : Dec prop

It was fairly easy from there to define structures and bundles up through commutative semirings.

Is this functionality already in agda-stdlib? A quick search for “IsMonoid” didn’t turn up anything obvious.

If this functionality isn’t already in agda-stdlib and if it sounds appealing to others, I’d be happy to package it for a PR, welcoming suggestions for its improvement in the process.

Comments?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/agda/agda-stdlib/issues/1404, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAP26EVDSZ3IEB7E44HDPJLS3DBEZANCNFSM4WNW2GGQ .

conal commented 3 years ago

Thanks for the reply, Matthew. I like this advice very much. There is another quite similar construction in my project, and hopefully I can unify them with the sort of generalization you’re suggesting.