laws for Decidable

[fommil]

in https://hackage.haskell.org/package/contravariant-1.4.1/docs/Data-Functor-Contravariant-Divisible.html#t:Decidable

"we expect the same kind of distributive law as is satisfied by the usual covariant Alternative, w.r.t Applicative, which should be fully formulated and added here at some point!"

could you please formalise this? I'd like to translate the laws to scalaz in scalaz/scalaz#1881

[ekmett]

Unfortunately, I rather deliberately didn't formalize it. Why? There are several forms of laws for Alternative vs. Applicative. e.g. Left catch vs. Left distribution from the MonadPlus reform proposal. Alternative is really 3-4 classes pretending to be one, just like MonadPlus, except the problem is slightly worse, since you don't have the implicit directional bias of Monad.

[fommil]

ok, say we're using the laws for Alt... what are the Decidable equivalents?

https://hackage.haskell.org/package/semigroupoids-5.2.2/docs/Data-Functor-Alt.html

    <!> is associative:             (a <!> b) <!> c = a <!> (b <!> c)
    <$> left-distributes over <!>:  f <$> (a <!> b) = (f <$> a) <!> (f <$> b)

[ekmett]

Note: even Alt admits that about half the instances only satisfy left-catch. ;) This also isn't terribly easily resolved as you often actually want to switch between those behaviors based on what you lift over. e.g. StateT String [] vs. StateT String Maybe have completely different behavior w.r.t those laws but both model different types of parser, so you can't just throw one of these or the other out.