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 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 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... : _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries