Skip to content

Instantly share code, notes, and snippets.

@yurrriq
Forked from ChrisPenner/TicTacToe.hs
Created August 23, 2017 07:35
Show Gist options
  • Save yurrriq/f120f0ece9cb6ece3f55169ac53bd0f1 to your computer and use it in GitHub Desktop.
Save yurrriq/f120f0ece9cb6ece3f55169ac53bd0f1 to your computer and use it in GitHub Desktop.
Type-safe game of TicTacToe
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language DeriveFunctor #-}
{-# language TypeInType #-}
{-# language UndecidableInstances #-}
{-# language ViewPatterns #-}
{-# language ConstraintKinds #-}
{-# language GADTs #-}
module TicTacToe where
import Data.Function ((&))
import GHC.TypeLits
data Trip a = Trip a a a
deriving (Show, Eq, Functor)
-- | Utility function to alter a value inside a triple
-- Can build get / set using `flip const ()` and `const x` respectively
overTrip :: CoordT -> (a -> a) -> Trip a -> Trip a
overTrip A f (Trip a b c) = Trip (f a) b c
overTrip B f (Trip a b c) = Trip a (f b) c
overTrip C f (Trip a b c) = Trip a b (f c)
-- | Keep a list of each Piece played and its location
data BoardRep = Empty
| Cons CoordT CoordT PieceT BoardRep
-- | Either X, O, or Nothing
data PieceT = X | O | N
deriving (Show, Eq)
-- | A proxy type which represents a piece
data Piece a where
X' :: Piece 'X
O' :: Piece 'O
N' :: Piece 'N
-- | Get the piece's actual value from a wrapper type
pieceVal :: Piece a -> PieceT
pieceVal X' = X
pieceVal O' = O
pieceVal N' = N
data CoordT = A | B | C
deriving (Show, Eq)
-- | A proxy type which represents a coordinate
data Coord (a :: CoordT) where
A' :: Coord 'A
B' :: Coord 'B
C' :: Coord 'C
-- | Get the coord's actual value from a wrapper type
coordVal :: Coord a -> CoordT
coordVal A' = A
coordVal B' = B
coordVal C' = C
-- | Is it the proper turn for p to play a piece?
type family IsTurn (p :: PieceT) (b :: BoardRep) where
IsTurn 'X b = Count 'X b ~ Count 'O b
IsTurn 'O b = Count 'X b ~ (Count 'O b + 1)
-- | Count amount of a certain piece on the board
type family Count (t :: PieceT) (l :: BoardRep) :: Nat where
Count _ 'Empty = 0
Count t ('Cons _ _ t rest) = 1 + Count t rest
Count t ('Cons _ _ _ rest) = Count t rest
-- | Has a square been played already?
type family Played (m :: CoordT) (n :: CoordT) (l :: BoardRep) :: Bool where
Played _ _ 'Empty = 'False
Played m n ('Cons m n _ _) = 'True
Played m n ('Cons _ _ _ rest) = Played m n rest
-- | A Board is a 3x3 vector
newtype Board x a = Board (Trip (Trip a))
deriving (Functor, Show, Eq)
-- | New empty board
newBoard :: Board 'Empty PieceT
newBoard = Board $ Trip (Trip N N N)
(Trip N N N)
(Trip N N N)
-- | Play a piece on square (m, n) if it's valid to do so
play ::
( IsTurn p b
, Played m n b ~ 'False
) => Piece p -> (Coord m, Coord n) -> Board b PieceT -> Board ('Cons m n p b) PieceT
play (pieceVal -> p) (coordVal -> x, coordVal -> y) (Board b) = Board $ overTrip y (overTrip x (const p)) b
-- | Clear any associated type info about the board
clearType :: Board b a -> Board () a
clearType (Board b) = Board b
game :: Board () PieceT
game = newBoard
& play X' (A', B')
& play O' (C', C')
& play X' (A', A')
& clearType
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment