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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

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

David Feuer
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
Reply | Threaded
Open this post in threaded view
|

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

Andreas Abel
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
Reply | Threaded
Open this post in threaded view
|

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

Oliver Charles-3
Refl, I believe.

On Thu, Jan 14, 2016 at 1:56 PM Andreas Abel <[hidden email]> wrote:
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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

David Feuer
In reply to this post by Andreas Abel

(:~:) is from Data.Type.Equality.

data a :~: b where
  Refl :: a :~: a

On Jan 14, 2016 8:56 AM, "Andreas Abel" <[hidden email]> wrote:
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
Reply | Threaded
Open this post in threaded view
|

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

Ryan Scott
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
Reply | Threaded
Open this post in threaded view
|

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

David Feuer
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
Reply | Threaded
Open this post in threaded view
|

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

Ryan Scott
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 <[hidden email]> 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 <[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