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. |
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. |
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. |
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
--------------------------------------------------------------------
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. |
Not only that, `xor` has inverses so it forms an abelian group
Regards, Andrew
--------------------------------------------------------------------
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. |
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. |
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. |
In reply to this post by Andrew Butterfield-2
xor a b = (a + b) mod 2 - Oleg On 29.9.2020 12.45, Andrew Butterfield
wrote:
Not only that, `xor` has inverses so it forms an abelian group _______________________________________________ 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. |
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. |
It's bitwise, so not that complicated
--------------------------------------------------------------------
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. |
In reply to this post by Mario Lang
But we're talking about xor for the Word64 type, so it is slightly more 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. |
Free forum by Nabble | Edit this page |