Skip to content

Instantly share code, notes, and snippets.

@mstksg
Last active August 26, 2017 23:58
Show Gist options
  • Save mstksg/a46c27a3ce091d5ad43bb7f4c3669a29 to your computer and use it in GitHub Desktop.
Save mstksg/a46c27a3ce091d5ad43bb7f4c3669a29 to your computer and use it in GitHub Desktop.
{-# language DeriveFunctor #-}
{-# language UndecidableInstances #-}
{-# language TypeInType #-}
{-# language TypeOperators #-}
{-# language TemplateHaskell #-}
{-# language KindSignatures #-}
{-# language DataKinds #-}
{-# language ViewPatterns #-}
{-# language GADTs #-}
{-# language TypeFamilies #-}
{-# language ScopedTypeVariables #-}
import Data.Function ((&))
import Data.Singletons.Prelude
import Data.Singletons.Prelude.List
import Data.Singletons.TH
-- | Either X or O
$(singletons [d|
data PieceT = X | O
deriving (Show, Eq)
data CoordT = A | B | C
deriving (Show, Eq)
|])
-- defines:
--
-- SX :: Sing 'X (or SPieceT 'X)
-- SO :: Sing 'O (or SPieceT 'O)
--
-- SA :: Sing 'A (or SCoordT 'A)
-- SB :: Sing 'B (or SCoordT 'B)
-- SC :: Sing 'C (or SCoordT 'C)
--
-- and also toSing, fromSing, etc.
type Coord = SCoordT
type Piece = SPieceT
-- | Get the coord's actual value from a singleton
coordVal :: Coord a -> CoordT
coordVal = fromSing
-- | Get the piece's actual value from a singleton
pieceVal :: Piece a -> PieceT
pieceVal = fromSing
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
type BoardRep = [(CoordT, CoordT, PieceT)]
-- A board is a 3x3 grid alongside its type representation
newtype Board (b :: BoardRep) a = Board (Trip (Trip (Maybe a)))
deriving (Show, Eq, Functor)
-- | New empty board
newBoard :: Board '[] PieceT
newBoard = Board $ Trip (Trip Nothing Nothing Nothing)
(Trip Nothing Nothing Nothing)
(Trip Nothing Nothing Nothing)
$(singletons [d|
-- | Has a square been played already?
played :: CoordT -> CoordT -> [(CoordT, CoordT, a)] -> Bool
played x y = any_ (\(x', y', _) -> x == x' && y == y')
|])
-- | Get who's turn it is
type family Turn (b :: BoardRep) :: PieceT where
Turn ('(_, _, 'X) ': _) = 'O
Turn _ = 'X
play
:: (Played x y b ~ 'False, Turn b ~ p)
=> Piece p
-> (Coord x, Coord y)
-> Board b PieceT
-> Board ('(x, y, p) ': b) PieceT
play (fromSing -> p) (fromSing -> x, fromSing -> y) (Board b)
= Board $ (overTrip y . overTrip x) (const (Just p)) b
-- | Play a piece on square (x, y) if it's valid to do so
playX :: (Played x y b ~ 'False, Turn b ~ 'X)
=> (Coord x, Coord y) -> Board b PieceT -> Board ('(x,y,'X) ': b) PieceT
playX = play SX
playO :: (Played x y b ~ 'False, Turn b ~ 'O)
=> (Coord x, Coord y) -> Board b PieceT -> Board ('(x,y,'O) ': b) PieceT
playO = play SO
game = newBoard
& play SX (SA, SB)
& play SO (SA, SA)
main :: IO ()
main = putStrLn "hi"
@mstksg
Copy link
Author

mstksg commented Aug 26, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment