Proposal: Add Semigroup and Monoid instances for (:~:)
david.feuer at gmail.com
Mon Jan 18 00:15:40 UTC 2016
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  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.
>  http://hackage.haskell.org/package/base-220.127.116.11/docs/Data-Type-Equality.html#t::-126-:
> Libraries mailing list
> Libraries at haskell.org
More information about the Libraries