Add newtype for Alternative using QuantifiedConstraints in base-4.13 (Libraries Digest, Vol 186, Issue 17)

Li-yao Xia lysxia at gmail.com
Tue Feb 19 15:20:17 UTC 2019


On 2/18/19 3:19 PM, Wolfgang Jeltsch wrote:
> If I remember correctly, then something that is an `Applicative` and a
> `Monoid` isnt necessarily an `Alternative` and something that is a
> `Monad` and a `Monoid` isnt necessarily a `MonadPlus`. There are
> certain axioms that are supposed to hold, which link the `Applicative`
> or `Monad` structure to the `Monoid` structure. At least this is how it
> ought to be. For details see the paper [From Monoids to Near-Semirings:
> The Essence of `MonadPlus` and `Alternative`][*].
> 
> [*]:
> � � https://usuarios.fceia.unr.edu.ar/~mauro/pubs/FromMonoidstoNearsemirings.pdf
>      "From Monoids to Near-Semirings: The Essence of `MonadPlus` and `Alternative`"
> 
> 


The laws studied by that paper are not universal to Alternative 
instances that occur in practice, and in fact I don't think it is 
possible to require anything more than a monoid structure from them.

Having only skimmed the paper, the only extra law not guaranteed by the 
proposed newtype seems to be the distributivity of join/(>>=) over (<|>) 
(equations 10 and 12 on page 6):

join (m1 <|> m2)   =   join m1 <|> join m2

or

(m1 <|> m2) >>= k   =   (m1 >>= k) <|> (m2 >>= k)

(I believe 9 and 11 must hold by parametricity (under reasonable 
conditions), hence they can be ignored.)

These equations are not satisfied by existing instances like Maybe and 
most parser monads (as noted in the paper), because it requires too much 
backtracking.

The paper mentions another, incompatible law (13 on page 7), that has 
also been studied elsewhere, and that one could push for:

pure a <|> b   =   pure a

But the ship has already sailed: there are plenty of Alternative 
instances in use that violate either (or possibly both) of these laws. 
Beyond a monoid structure, I don't know any other law that can be 
uncontroversially expected from Alternative instances. If indeed no 
other universal requirement can be found, the proposed newtype is 
acceptable from the point of view of laws.

It might be better to document those extra laws in a non-prescriptive 
fashion, to tell users of Alternative that "it might be enlightening to 
consider whether your functor satisfies those laws".

Regards,
Li-yao


More information about the Libraries mailing list