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

Ryan Scott at
Mon Jan 18 00:02:42 UTC 2016

+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.

More information about the Libraries mailing list