I think I discovered my first Monoid instance

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

I think I discovered my first Monoid instance

Mario Lang
Hi.

A common theme of some Haskell talks seems to be to motivate people to
go and hunt for instances of standard typeclasses.  As the hobbyist
Haskell programmer that I am, I kept on wondering if I would
ever find some.  It feels sort of unrealistic, or at least unlikely,
that I should suddenly start to see meaningful structure in
code just because I think I know some typeclasses.

I think I finally discovered a Monoid instance that helps to express a
concept in code pretty well.  However, unsure about the soundness of my
blundering about, I'd like to confirm (or disprove!) my findings
before I fall in love with the approach too much.

In my chess library (chessIO) I use bitboards to represent chess positions.

data QuadBitboard = QBB { black :: {-# UNPACK #-} !Word64
                        , pbq :: {-# UNPACK #-} !Word64
                        , nbk :: {-# UNPACK #-} !Word64
                        , rqk :: {-# UNPACK #-} !Word64
                        } deriving (Eq)

A quad bitboard is a space optimisation based on the observation
that a square can only be occupied by one piece.

occupied QBB{pbq, nbk, rqk} = pbq  .|.  nbk  .|.  rqk
pnr      QBB{pbq, nbk, rqk} = pbq `xor` nbk `xor` rqk
white                       = liftA2 xor occupied black
pawns                       = liftA2 (.&.) pnr pbq
knights                     = liftA2 (.&.) pnr nbk
bishops                     = liftA2 (.&.) pbq nbk
rooks                       = liftA2 (.&.) pnr rqk
queens                      = liftA2 (.&.) pbq rqk
kings                       = liftA2 (.&.) nbk rqk

We can create a bitboard with a single occupied square:

square :: Int -> Word4 -> QuadBitboard
square !sq !nb = QBB (f 0) (f 1) (f 2) (f 3) where
  !b = bit sq
  f !n = fromIntegral ((nb `unsafeShiftR` n) .&. 1) * b

And, as an aside, we can even use pattern synonyms to give these nibbles
meaningful names.

pattern NoPiece     = 0
pattern WhitePawn   = 2
pattern WhiteKnight = 4
pattern WhiteBishop = 6
pattern WhiteRook   = 8
pattern WhiteQueen  = 10
pattern WhiteKing   = 12
pattern BlackPawn   = 3
pattern BlackKnight = 5
pattern BlackBishop = 7
pattern BlackRook   = 9
pattern BlackQueen  = 11
pattern BlackKing   = 13

But what felt really like a cool discovery, is combination:

instance Monoid QuadBitboard where
  mempty = QBB 0 0 0 0

-- | bitwise XOR
instance Semigroup QuadBitboard where
  QBB b0 b1 b2 b3 <> QBB b0' b1' b2' b3' =
    QBB (b0 `xor` b0') (b1 `xor` b1') (b2 `xor` b2') (b3 `xor` b3')

With this, we can pretty easily define a function to create a quad
bitboard from a string:

instance IsString QuadBitboard where
  fromString = go (7, 0) mempty where
    go _ !qbb "" = qbb
    go (!r,_) qbb ('/':xs) = go (r - 1, 0) qbb xs
    go (!r,!f) !qbb (x:xs)
      | inRange ('1','8') x = go (r, f + (ord x - ord '0')) qbb xs
      | otherwise = go (r, f + 1) (qbb <> square (r*8+f) nb) xs where
        nb = case x of
          'P' -> WhitePawn
          'N' -> WhiteKnight
          'B' -> WhiteBishop
          'R' -> WhiteRook
          'Q' -> WhiteQueen
          'K' -> WhiteKing
          'p' -> BlackPawn
          'n' -> BlackKnight
          'b' -> BlackBishop
          'r' -> BlackRook
          'q' -> BlackQueen
          'k' -> BlackKing
          _ -> error $ "QuadBitBoard.fromString: Illegal FEN character " <> show x

standard :: QuadBitboard
standard = "rnbqkbnr/pppppppp/8/8/8/8/PPPPPPPP/RNBQKBNR"

The rest of the module builds on the Monoid instance of QuadBitboard.

Again, this is the first time a instance like this turns up in my Haskell
experiments.  It feels extremely satisfying having discovered this. But
maybe I am violating some laws (I hear instances do that sometimes!) or
some other thing is totally wrong.  One might say
I am not fully trusting the peace.

https://hackage.haskell.org/package/chessIO/docs/Game-Chess-QuadBitboard.html

--
CYa,
  ⡍⠁⠗⠊⠕
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Ben Franksen
Am 29.09.20 um 10:27 schrieb Mario Lang:
> instance Monoid QuadBitboard where
>   mempty = QBB 0 0 0 0
>
> -- | bitwise XOR
> instance Semigroup QuadBitboard where
>   QBB b0 b1 b2 b3 <> QBB b0' b1' b2' b3' =
>     QBB (b0 `xor` b0') (b1 `xor` b1') (b2 `xor` b2') (b3 `xor` b3')
>
> But maybe I am violating some laws

The Semigroup is okay, since 'xor' is indeed associative, and your
instance basically lifts it to 4-tuples.

The Monoid instance is wrong, though. There is no unit for 'xor'!

Cheers
Ben

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Henning Thielemann

On Tue, 29 Sep 2020, Ben Franksen wrote:

> Am 29.09.20 um 10:27 schrieb Mario Lang:
>> instance Monoid QuadBitboard where
>>   mempty = QBB 0 0 0 0
>>
>> -- | bitwise XOR
>> instance Semigroup QuadBitboard where
>>   QBB b0 b1 b2 b3 <> QBB b0' b1' b2' b3' =
>>     QBB (b0 `xor` b0') (b1 `xor` b1') (b2 `xor` b2') (b3 `xor` b3')
>>
>> But maybe I am violating some laws
>
> The Semigroup is okay, since 'xor' is indeed associative, and your
> instance basically lifts it to 4-tuples.
>
> The Monoid instance is wrong, though. There is no unit for 'xor'!

Why should 0 not be the identity element?
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Andrew Butterfield-2
In reply to this post by Ben Franksen
Hmmm - I thought so at first

A B A `xor` B
0 0      0
0 1      1
1 0      1
1 1      0

0 `xor` b = b
a `xor` 0 = a

Looks like 0 is the identity to me.

Regards, Andrew

On 29 Sep 2020, at 10:33, Ben Franksen <[hidden email]> wrote:

Am 29.09.20 um 10:27 schrieb Mario Lang:
instance Monoid QuadBitboard where
 mempty = QBB 0 0 0 0

-- | bitwise XOR
instance Semigroup QuadBitboard where
 QBB b0 b1 b2 b3 <> QBB b0' b1' b2' b3' =
   QBB (b0 `xor` b0') (b1 `xor` b1') (b2 `xor` b2') (b3 `xor` b3')

But maybe I am violating some laws

The Semigroup is okay, since 'xor' is indeed associative, and your
instance basically lifts it to 4-tuples.

The Monoid instance is wrong, though. There is no unit for 'xor'!

Cheers
Ben

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Andrew Butterfield-2
Not only that, `xor` has inverses so it forms an abelian group

Regards, Andrew

On 29 Sep 2020, at 10:41, Andrew Butterfield <[hidden email]> wrote:

Hmmm - I thought so at first

A B A `xor` B
0 0      0
0 1      1
1 0      1
1 1      0

0 `xor` b = b
a `xor` 0 = a

Looks like 0 is the identity to me.

Regards, Andrew

On 29 Sep 2020, at 10:33, Ben Franksen <[hidden email]> wrote:

Am 29.09.20 um 10:27 schrieb Mario Lang:
instance Monoid QuadBitboard where
 mempty = QBB 0 0 0 0

-- | bitwise XOR
instance Semigroup QuadBitboard where
 QBB b0 b1 b2 b3 <> QBB b0' b1' b2' b3' =
   QBB (b0 `xor` b0') (b1 `xor` b1') (b2 `xor` b2') (b3 `xor` b3')

But maybe I am violating some laws

The Semigroup is okay, since 'xor' is indeed associative, and your
instance basically lifts it to 4-tuples.

The Monoid instance is wrong, though. There is no unit for 'xor'!

Cheers
Ben

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Ben Franksen
In reply to this post by Henning Thielemann
Am 29.09.20 um 11:38 schrieb Henning Thielemann:

>
> On Tue, 29 Sep 2020, Ben Franksen wrote:
>
>> Am 29.09.20 um 10:27 schrieb Mario Lang:
>>> instance Monoid QuadBitboard where
>>>   mempty = QBB 0 0 0 0
>>>
>>> -- | bitwise XOR
>>> instance Semigroup QuadBitboard where
>>>   QBB b0 b1 b2 b3 <> QBB b0' b1' b2' b3' =
>>>     QBB (b0 `xor` b0') (b1 `xor` b1') (b2 `xor` b2') (b3 `xor` b3')
>>>
>>> But maybe I am violating some laws
>>
>> The Semigroup is okay, since 'xor' is indeed associative, and your
>> instance basically lifts it to 4-tuples.
>>
>> The Monoid instance is wrong, though. There is no unit for 'xor'!
>
> Why should 0 not be the identity element?

Sorry, i was confused. Indeed 0 is a unit. The Monoid instance is lawful.

Cheers
Ben

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Henning Thielemann
In reply to this post by Andrew Butterfield-2

On Tue, 29 Sep 2020, Andrew Butterfield wrote:

> Not only that, `xor` has inverses so it forms an abelian group

... and it's no surprise since 'xor' is '+' in ℤ₂.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Oleg Grenrus
In reply to this post by Andrew Butterfield-2

xor a b = (a + b) mod 2

Many good properties follow. https://en.wikipedia.org/wiki/GF(2) ...

- Oleg

On 29.9.2020 12.45, Andrew Butterfield wrote:
Not only that, `xor` has inverses so it forms an abelian group

Regards, Andrew

On 29 Sep 2020, at 10:41, Andrew Butterfield <[hidden email]> wrote:

Hmmm - I thought so at first

A B A `xor` B
0 0      0
0 1      1
1 0      1
1 1      0

0 `xor` b = b
a `xor` 0 = a

Looks like 0 is the identity to me.

Regards, Andrew

On 29 Sep 2020, at 10:33, Ben Franksen <[hidden email]> wrote:

Am 29.09.20 um 10:27 schrieb Mario Lang:
instance Monoid QuadBitboard where
 mempty = QBB 0 0 0 0

-- | bitwise XOR
instance Semigroup QuadBitboard where
 QBB b0 b1 b2 b3 <> QBB b0' b1' b2' b3' =
   QBB (b0 `xor` b0') (b1 `xor` b1') (b2 `xor` b2') (b3 `xor` b3')

But maybe I am violating some laws

The Semigroup is okay, since 'xor' is indeed associative, and your
instance basically lifts it to 4-tuples.

The Monoid instance is wrong, though. There is no unit for 'xor'!

Cheers
Ben

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Jaro Reinders
In reply to this post by Henning Thielemann
But we're talking about xor for the Word64 type, so it is slightly more
complicated to prove that it has a unit.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

Andrew Butterfield-2
It's bitwise, so not that complicated

On 29 Sep 2020, at 10:52, Jaro Reinders <[hidden email]> wrote:

But we're talking about xor for the Word64 type, so it is slightly more
complicated to prove that it has a unit.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: I think I discovered my first Monoid instance

David Banas-2
In reply to this post by Mario Lang
But we're talking about xor for the Word64 type, so it is slightly more
complicated to prove that it has a unit.

Here's a proof in Agda:

-- Agda proof that zero is the unit (i.e. - left and right identity)
-- for the XOR operation.

import Relation.Binary.PropositionalEquality as Eq
open        Eq       using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

-- Binary data.

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

_xor_ : Bin → Bin → Bin
⟨⟩    xor y      =  y
(x O) xor ⟨⟩     =  x O
(x O) xor (y O)  = (x xor y) O
(x O) xor (y I)  = (x xor y) I
(x I) xor ⟨⟩     =  x I
(x I) xor (y O)  = (x xor y) I
(x I) xor (y I)  = (x xor y) O

lemma : ∀ (b : Bin)
    ------------
  → b xor ⟨⟩ ≡ b
lemma ⟨⟩    = refl
lemma (b O) = refl
lemma (b I) = refl
 
_ : ( ⟨⟩ I O O I O I I O )  xor
    ( ⟨⟩ O I I I O O O O )
    ----------------------
  ≡ ( ⟨⟩ I I I O O I I O )
_ = refl

-- Left & right identity proofs.
postulate
  binO : (⟨⟩ O) ≡ ⟨⟩  -- Just accomodating a syntactical nuisance.

xor-idₗ : ∀ (b : Bin)
    ----------------
  → (⟨⟩ O) xor b ≡ b
xor-idₗ ⟨⟩ rewrite binO  =  refl
xor-idₗ (b O)            =  refl
xor-idₗ (b I)            =  refl

xor-idᵣ : ∀ (b : Bin)
    ----------------
  → b xor (⟨⟩ O) ≡ b
xor-idᵣ ⟨⟩    rewrite binO     =  refl
xor-idᵣ (b O) rewrite lemma b  =  refl
xor-idᵣ (b I) rewrite lemma b  =  refl

-db


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.