<div dir="ltr"><div><div>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.<br><br></div>Unconditional +1 from me.<br><br></div>Ryan S.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 17, 2016 at 7:15 PM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">The definitions I gave for <> and mappend are each strict in the left<br>
argument, which is enough to ensure soundness--if  (x :: a :~: b) <><br>
(y :: a :~: b) is not bottom, then surely x is not bottom, so a :~: b.<br>
So this is really only a question of efficiency. I don't have a very<br>
strong opinion myself, but I think we might be better off leaving<br>
things lazy in the second argument.<br>
<div><div class="h5"><br>
On Sun, Jan 17, 2016 at 7:02 PM, Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com">ryan.gl.scott@gmail.com</a>> wrote:<br>
> +1, with a one stipulation: I'd rather the Semigroup instance be:<br>
><br>
>     instance Semigroup (a :~: b) where<br>
>       Refl <> Refl = Refl<br>
><br>
> and similarly for Monoid(mappend). It's a minor quibble, but the<br>
> documentation [1] for (:~:) says that there's only a proof term for a<br>
> ~ b if it's inhabited by a terminating value, so performing a strict<br>
> pattern match seems like the best default here.<br>
><br>
> Ryan S.<br>
> -----<br>
> [1] <a href="http://hackage.haskell.org/package/base-4.8.1.0/docs/Data-Type-Equality.html#t::-126-" rel="noreferrer" target="_blank">http://hackage.haskell.org/package/base-4.8.1.0/docs/Data-Type-Equality.html#t::-126-</a>:<br>
</div></div>> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div><br></div>