These are not likely to be *useful*, but they fall easily into the
general bucket of "exactly one sensible instance exists". instance Semigroup (a :~: b) where r <> _ = r instance a ~ b => Monoid (a :~: b) where mempty = Refl mappend r _ = r _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
What does this smiley :~: stand for?
On 13.01.2016 06:58, David Feuer wrote: > These are not likely to be *useful*, but they fall easily into the > general bucket of "exactly one sensible instance exists". > > instance Semigroup (a :~: b) where > r <> _ = r > > instance a ~ b => Monoid (a :~: b) where > mempty = Refl > mappend r _ = r > _______________________________________________ > Libraries mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden [hidden email] http://www2.tcs.ifi.lmu.de/~abel/ _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Refl, I believe. On Thu, Jan 14, 2016 at 1:56 PM Andreas Abel <[hidden email]> wrote: What does this smiley :~: stand for? _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Andreas Abel
(:~:) is from Data.Type.Equality. data a :~: b where On Jan 14, 2016 8:56 AM, "Andreas Abel" <[hidden email]> wrote:
What does this smiley :~: stand for? _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by David Feuer
+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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> 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 > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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.On Sun, Jan 17, 2016 at 7:15 PM, David Feuer <[hidden email]> wrote: The definitions I gave for <> and mappend are each strict in the left _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Free forum by Nabble | Edit this page |