search

ekmett / contravariant

Haskell 98 contravariant functors
http://hackage.haskell.org/package/contravariant
Other
73 stars 24 forks source link

Divisible/Decidable Laws #10

Closed maxsnew closed 9 years ago

maxsnew commented 9 years ago

An attempt to express the absorption and distributive laws. The f' definition is really ugly, but I think the laws are right.

Absorption wasn't mentioned in the documentation before. Is it redundant? I know it is for rings, but I think you need additive inverses to prove it.

ekmett commented 9 years ago

The main reason I'd avoided diving into the laws expressing their relationship was for fear of stepping into a 'Alternative'/'MonadPlus' law hell where the actual laws are actually quite messy. They appear to really be multiple classes in disguise. Not sure how much Divisible/Decidable run into the same issue.

I'm happy to leave this thread open to hash these out, but I'm loathe to just click 'merge' here without thought.

maxsnew commented 9 years ago

Hm, any link to a good overview of the Alternative/MonadPlus stuff? Is the issue with those just that there have to be laws wrt how <|> interacts with >>= and such, in which case we don't have that problem here?

I just translated the right-seminearring laws to carry the extra functions around. I guess you're saying that not even that is agreed upon? I took the line in the current docs to mean that no one had bothered to do it yet, not that it was uncertain what the laws really were.

ekmett commented 9 years ago

The right seminearring laws already don't hold for Alternative. It is dangerous to assume they'd hold universally for a contravariant version

ekmett commented 9 years ago

Skim http://www.reddit.com/r/haskell/comments/2tfgol/alternatives_convert_products_to_sums/cnynnyt for a brief-ish summary of the kinds of issues that arise.

ekmett commented 9 years ago

I merged the doc-fix parts. I'm going to close this out though, as we don't actually have a known-good distributive law in the presence of users using things like Alternative to make it go.