Proposal: Add Semigroup and Monoid instances for (:~:)

[David Feuer]

The definitions I gave for <> and mappend are each strict in the left
argument, which is enough to ensure soundness--if  (x :: a :~: b) <>
(y :: a :~: b) is not bottom, then surely x is not bottom, so a :~: b.
So this is really only a question of efficiency. I don't have a very
strong opinion myself, but I think we might be better off leaving
things lazy in the second argument.

On Sun, Jan 17, 2016 at 7:02 PM, Ryan Scott <ryan.gl.scott at gmail.com> wrote:
> +1, with a one stipulation: I'd rather the Semigroup instance be:
>
>     instance Semigroup (a :~: b) where
>       Refl <> Refl = Refl
>
> and similarly for Monoid(mappend). It's a minor quibble, but the
> documentation [1] for (:~:) says that there's only a proof term for a
> ~ b if it's inhabited by a terminating value, so performing a strict
> pattern match seems like the best default here.
>
> Ryan S.
> -----
> [1] http://hackage.haskell.org/package/base-4.8.1.0/docs/Data-Type-Equality.html#t::-126-:
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries