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

[Ryan Scott]

OK, you (and Eric Mertens) have convinced me. I was originally put off by
the fact that r <> _ = r is (technically) lazy, but you'd still need to
strictly pattern-match on the result anyway in order to bring evidence that
a ~ b into scope, so it's not an issue like I thought it was.

Unconditional +1 from me.

Ryan S.

On Sun, Jan 17, 2016 at 7:15 PM, David Feuer <david.feuer at gmail.com> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20160117/01f9b483/attachment.html>