diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for sized-grid + +## 0.1.0.0 -- 2018-04-18 + +* First version. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2018 edwardwas + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.lhs b/README.lhs new file mode 100644 --- /dev/null +++ b/README.lhs @@ -0,0 +1,164 @@ +[![Build Status](https://travis-ci.org/edwardwas/sized-grid.svg?branch=master)](https://travis-ci.org/edwardwas/sized-grid) + +sized-grid +=========== + +A way of working with grids in Haskell with size encoded at the type level. + +Quick tutorial +======== + +The core datatype of this library is `Grid (cs :: '[k]) (a :: *)`. `cs` is a type level list of coordinate types. We could use a single type level number here, but by using different types we can say what happened when we move outside the bounds of a grid. There are three different coordinate types provided. + +* `Ordinal n`: An ordinal can be an integral number between 0 and n - 1. As numbers outside the grid are not possible, this has the most restrictive API. One can convert between an Ordinal and a number of ordinalToNum and numToOrdinal. + +* `HardWrap n`: Like Oridnal, HardWrap can only hold intergral numbers between 0 and n - 1, but it allows a more permissive API by clamping values outside of its range. It is an instance of `Semigroup` and `Monoid`, where `mempty` is 0 and `<>` is addition. + +* `Periodic n`: This is the most permissive. When a value is generated outside the given range, it wraps that around using modular arithmetic. Is is an instance of `Semigroup` and `Monoid` like `HardWrap`, but also of `AdditiveGroup` allowing negation. + +`HardWrap` and `Periodic` are both instances of `AffineSpace`, with their `Diff` being `Integer`. This means there are many occasions where one doesn't have to work directly with these values (which can be cumbersome) and can instead work with their differences as regular numbers. + +The last type value of `Grid` is the type of each element. + +The other main type is `Coord cs`, where `cs` is, again, a type level list of coordinate types. For example, `Coord '[Periodic 3, HardWrap 4]` is a coordinate in a 3 by 4 2D space. The different types (`Periodic` and `HardWrap`) tell how to handle combining theses different numbers. `Coord cs` is an instance of `Semigroup`, `Monoid` and `AdditiveGroup` as long as each of the coordinates is also an instance of that typeclass. `Coord` is also an instance of of `AffineSpace`, where `Diff` is a n-tuple, meaning we can pattern match and do all sorts of nice things. + +There is a deliberately small number of functions that work over `Grid`: we instead opt for using typeclasses to create the required functionality. `Grid` is an instance of the following types (with some required constraints): + +* `Functor`: Update all values in the grid with the same function +* `Applicative`: As the size of the grid is statically known, `pure` just creates a grid with the same element at each point. `<*>` combines the grids point wise. +* `Monad`: I'm not sure if there is much of a need for this, but an instance exists. +* `Foldable`: Combine each element of the grid +* `Traverse`: Apply an applicative function over the grid +* `IndexedFunctor`, `IndexedFoldable` and `IndexedTraversable`: Like `Functor`, `Foldable` and `Traversable`, but with access to the position at each point. These are from the lens package +* `Distributive`: Like `Traversable`, but the other way round. Allows us to put a functor inside the grid +* `Representable`: `Grid cs a` is isomorphic `Coord cs -> a`, so we can `tabulate` and `index` to make this conversion + +We also have a `FocusedGrid` type, which is like `Grid` but has a certain focused position. This means that we lose many instances, but we gain `Comonad` and `ComonadStore`. + +When dealing with areas around `Coord`s, we can use `moorePoints` and `vonNeumanPoints` to generate [Moore](https://en.wikipedia.org/wiki/Moore_neighborhood) and [von Neuman](https://en.wikipedia.org/wiki/Von_Neumann_neighborhood) neighbourhoods. Note that these include the center point. + +We introduce two new typeclasses: `IsCoord` and `IsGrid`. `IsGrid` has `gridIndex`, which allows us to get a single element of the grid and lenses to convert between `FocusedGrid` and `Grid`. `IsCoord` has `CoordSized`, which is the size of the coord and an iso to convert between `Ordinal` and the `Coord`. + +Example - Game of Life +===================== + +As is traditional for anything with grids and comonads in Haskell, we can reimplement [Conway's Game of Life](https://en.wikipedia.org/wiki/Conway%27s_Game_of_Life). + +This is a literate Haskell file, so we start by turning on some language extensions, importing our library and some other utilities. + +```haskell +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE DataKinds #-} + +import SizedGrid + +import Control.Comonad +import Control.Lens +import Control.Comonad.Store +import Data.AdditiveGroup +import Data.AffineSpace +import Data.Distributive +import Data.Functor.Rep +import Data.Semigroup (Semigroup(..)) +import GHC.TypeLits +import System.Console.ANSI +``` + +We create a datatype for alive or dead. + +```haskell +data TileState = Alive | Dead deriving (Eq,Show) +``` + +We encode the rules of the game via a step function. + +```haskell +type Rule = TileState -> [TileState] -> TileState + +gameOfLife :: Rule +gameOfLife here neigh = + let aliveNeigh = length $ filter (== Alive) neigh + in if | here == Alive && aliveNeigh `elem` [2,3] -> Alive + | here == Dead && aliveNeigh == 3 -> Alive + | otherwise -> Dead +``` + +We can then write a function to apply this to every point in a grid. + +```haskell +applyRule :: + ( All IsCoord cs + , All Monoid cs + , All Semigroup cs + , All AffineSpace cs + , All Eq cs + , AllDiffSame Integer cs + , KnownNat (MaxCoordSize cs) + , IsGrid cs (grid cs) + ) + => Rule + -> grid cs TileState + -> grid cs TileState +applyRule rule = over asFocusedGrid $ + extend $ \fg -> rule (extract fg) $ map (\p -> peek p fg) $ + filter (/= pos fg) $ moorePoints (1 :: Integer) $ pos fg + +``` + +We can create a simple drawing function to display it to the screen. + +```haskell +displayTileState :: TileState -> Char +displayTileState Alive = '#' +displayTileState Dead = '.' + +displayGrid :: (KnownNat (CoordSized x), KnownNat (CoordSized y)) => + Grid '[x, y] TileState -> String +displayGrid = unlines . collapseGrid . fmap displayTileState +``` + +Let's create a glider, and watch it move! + +```haskell +glider :: + ( KnownNat (CoordSized x * CoordSized y) + , Semigroup x + , Semigroup y + , Monoid x + , Monoid y + , IsCoord x + , IsCoord y + , AffineSpace x + , AffineSpace y + , Diff x ~ Integer + , Diff y ~ Integer + ) + => Coord '[x,y] + -> Grid '[x,y] TileState +glider offset = pure Dead + & gridIndex (offset .+^ (0,-1)) .~ Alive + & gridIndex (offset .+^ (1,0)) .~ Alive + & gridIndex (offset .+^ (-1,1)) .~ Alive + & gridIndex (offset .+^ (0,1)) .~ Alive + & gridIndex (offset .+^ (1,1)) .~ Alive +``` + +We can now make our glider run! + +```haskell +run = + let start :: Grid '[Periodic 10, Periodic 10] TileState + start = glider (mempty .+^ (3,3)) + doStep grid = do + clearScreen + putStrLn $ displayGrid grid + _ <- getLine + doStep $ applyRule gameOfLife grid + in doStep start + +main = return () +``` diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,164 @@ +[![Build Status](https://travis-ci.org/edwardwas/sized-grid.svg?branch=master)](https://travis-ci.org/edwardwas/sized-grid) + +sized-grid +=========== + +A way of working with grids in Haskell with size encoded at the type level. + +Quick tutorial +======== + +The core datatype of this library is `Grid (cs :: '[k]) (a :: *)`. `cs` is a type level list of coordinate types. We could use a single type level number here, but by using different types we can say what happened when we move outside the bounds of a grid. There are three different coordinate types provided. + +* `Ordinal n`: An ordinal can be an integral number between 0 and n - 1. As numbers outside the grid are not possible, this has the most restrictive API. One can convert between an Ordinal and a number of ordinalToNum and numToOrdinal. + +* `HardWrap n`: Like Oridnal, HardWrap can only hold intergral numbers between 0 and n - 1, but it allows a more permissive API by clamping values outside of its range. It is an instance of `Semigroup` and `Monoid`, where `mempty` is 0 and `<>` is addition. + +* `Periodic n`: This is the most permissive. When a value is generated outside the given range, it wraps that around using modular arithmetic. Is is an instance of `Semigroup` and `Monoid` like `HardWrap`, but also of `AdditiveGroup` allowing negation. + +`HardWrap` and `Periodic` are both instances of `AffineSpace`, with their `Diff` being `Integer`. This means there are many occasions where one doesn't have to work directly with these values (which can be cumbersome) and can instead work with their differences as regular numbers. + +The last type value of `Grid` is the type of each element. + +The other main type is `Coord cs`, where `cs` is, again, a type level list of coordinate types. For example, `Coord '[Periodic 3, HardWrap 4]` is a coordinate in a 3 by 4 2D space. The different types (`Periodic` and `HardWrap`) tell how to handle combining theses different numbers. `Coord cs` is an instance of `Semigroup`, `Monoid` and `AdditiveGroup` as long as each of the coordinates is also an instance of that typeclass. `Coord` is also an instance of of `AffineSpace`, where `Diff` is a n-tuple, meaning we can pattern match and do all sorts of nice things. + +There is a deliberately small number of functions that work over `Grid`: we instead opt for using typeclasses to create the required functionality. `Grid` is an instance of the following types (with some required constraints): + +* `Functor`: Update all values in the grid with the same function +* `Applicative`: As the size of the grid is statically known, `pure` just creates a grid with the same element at each point. `<*>` combines the grids point wise. +* `Monad`: I'm not sure if there is much of a need for this, but an instance exists. +* `Foldable`: Combine each element of the grid +* `Traverse`: Apply an applicative function over the grid +* `IndexedFunctor`, `IndexedFoldable` and `IndexedTraversable`: Like `Functor`, `Foldable` and `Traversable`, but with access to the position at each point. These are from the lens package +* `Distributive`: Like `Traversable`, but the other way round. Allows us to put a functor inside the grid +* `Representable`: `Grid cs a` is isomorphic `Coord cs -> a`, so we can `tabulate` and `index` to make this conversion + +We also have a `FocusedGrid` type, which is like `Grid` but has a certain focused position. This means that we lose many instances, but we gain `Comonad` and `ComonadStore`. + +When dealing with areas around `Coord`s, we can use `moorePoints` and `vonNeumanPoints` to generate [Moore](https://en.wikipedia.org/wiki/Moore_neighborhood) and [von Neuman](https://en.wikipedia.org/wiki/Von_Neumann_neighborhood) neighbourhoods. Note that these include the center point. + +We introduce two new typeclasses: `IsCoord` and `IsGrid`. `IsGrid` has `gridIndex`, which allows us to get a single element of the grid and lenses to convert between `FocusedGrid` and `Grid`. `IsCoord` has `CoordSized`, which is the size of the coord and an iso to convert between `Ordinal` and the `Coord`. + +Example - Game of Life +===================== + +As is traditional for anything with grids and comonads in Haskell, we can reimplement [Conway's Game of Life](https://en.wikipedia.org/wiki/Conway%27s_Game_of_Life). + +This is a literate Haskell file, so we start by turning on some language extensions, importing our library and some other utilities. + +```haskell +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE DataKinds #-} + +import SizedGrid + +import Control.Comonad +import Control.Lens +import Control.Comonad.Store +import Data.AdditiveGroup +import Data.AffineSpace +import Data.Distributive +import Data.Functor.Rep +import Data.Semigroup (Semigroup(..)) +import GHC.TypeLits +import System.Console.ANSI +``` + +We create a datatype for alive or dead. + +```haskell +data TileState = Alive | Dead deriving (Eq,Show) +``` + +We encode the rules of the game via a step function. + +```haskell +type Rule = TileState -> [TileState] -> TileState + +gameOfLife :: Rule +gameOfLife here neigh = + let aliveNeigh = length $ filter (== Alive) neigh + in if | here == Alive && aliveNeigh `elem` [2,3] -> Alive + | here == Dead && aliveNeigh == 3 -> Alive + | otherwise -> Dead +``` + +We can then write a function to apply this to every point in a grid. + +```haskell +applyRule :: + ( All IsCoord cs + , All Monoid cs + , All Semigroup cs + , All AffineSpace cs + , All Eq cs + , AllDiffSame Integer cs + , KnownNat (MaxCoordSize cs) + , IsGrid cs (grid cs) + ) + => Rule + -> grid cs TileState + -> grid cs TileState +applyRule rule = over asFocusedGrid $ + extend $ \fg -> rule (extract fg) $ map (\p -> peek p fg) $ + filter (/= pos fg) $ moorePoints (1 :: Integer) $ pos fg + +``` + +We can create a simple drawing function to display it to the screen. + +```haskell +displayTileState :: TileState -> Char +displayTileState Alive = '#' +displayTileState Dead = '.' + +displayGrid :: (KnownNat (CoordSized x), KnownNat (CoordSized y)) => + Grid '[x, y] TileState -> String +displayGrid = unlines . collapseGrid . fmap displayTileState +``` + +Let's create a glider, and watch it move! + +```haskell +glider :: + ( KnownNat (CoordSized x * CoordSized y) + , Semigroup x + , Semigroup y + , Monoid x + , Monoid y + , IsCoord x + , IsCoord y + , AffineSpace x + , AffineSpace y + , Diff x ~ Integer + , Diff y ~ Integer + ) + => Coord '[x,y] + -> Grid '[x,y] TileState +glider offset = pure Dead + & gridIndex (offset .+^ (0,-1)) .~ Alive + & gridIndex (offset .+^ (1,0)) .~ Alive + & gridIndex (offset .+^ (-1,1)) .~ Alive + & gridIndex (offset .+^ (0,1)) .~ Alive + & gridIndex (offset .+^ (1,1)) .~ Alive +``` + +We can now make our glider run! + +```haskell +run = + let start :: Grid '[Periodic 10, Periodic 10] TileState + start = glider (mempty .+^ (3,3)) + doStep grid = do + clearScreen + putStrLn $ displayGrid grid + _ <- getLine + doStep $ applyRule gameOfLife grid + in doStep start + +main = return () +``` diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/sized-grid.cabal b/sized-grid.cabal new file mode 100644 --- /dev/null +++ b/sized-grid.cabal @@ -0,0 +1,86 @@ +name: sized-grid +version: 0.1.0.0 +cabal-version: >=1.10 +category: Data +build-type: Simple +license: MIT +license-file: LICENSE +maintainer: ed@wastell.co.uk +bug-reports: https://github.com/edwardwas/sized-grid/issues +synopsis: Multidimensional grids with sized specified at compile time +author: edwardwas +homepage: https://github.com/edwardwas/sized-grid +description: + `size-grid` allows you to make finite sized grids and have their size and shape confirmed at compile time + . + Consult the readme for a short tutorial and explanation. +extra-source-files: + ChangeLog.md + README.lhs + README.md + +library + exposed-modules: + SizedGrid.Ordinal + SizedGrid.Coord + SizedGrid.Coord.Class + SizedGrid.Coord.Periodic + SizedGrid.Coord.HardWrap + SizedGrid.Grid.Class + SizedGrid.Grid.Grid + SizedGrid.Grid.Focused + SizedGrid + build-depends: + base >=4.8 && <4.12, + lens >=4.16.1 && <4.17, + vector >=0.12.0.1 && <0.13, + vector-space ==0.13.*, + generics-sop >=0.3.2.0 && <0.4, + distributive >=0.5.3 && <0.6, + adjunctions ==4.4.*, + comonad >=5.0.3 && <5.1, + random ==1.1.*, + mtl >=2.2.2 && <2.3, + constraints ==0.10.*, + aeson >=1.2.4.0 && <1.3 + default-language: Haskell2010 + hs-source-dirs: src + other-modules: + SizedGrid.Internal.Type + ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints + +test-suite tests + type: exitcode-stdio-1.0 + main-is: Main.hs + build-depends: + base >=4.8 && <4.12, + sized-grid -any, + hedgehog >=0.5.3 && <0.6, + tasty >=1.0.1.1 && <1.1, + tasty-hedgehog >=0.1.0.2 && <0.2, + vector-space ==0.13.*, + generics-sop >=0.3.2.0 && <0.4, + lens >=4.16.1 && <4.17, + adjunctions ==4.4.*, + aeson >=1.2.4.0 && <1.3, + HUnit >=1.6.0.0 && <1.7, + tasty-hunit >=0.10.0.1 && <0.11 + default-language: Haskell2010 + hs-source-dirs: tests + other-modules: + Test.Utils +test-suite readme + type: exitcode-stdio-1.0 + main-is: README.lhs + build-depends: + base >=4.10.1.0 && <4.11, + markdown-unlit >=0.5.0 && <0.6, + sized-grid -any, + distributive >=0.5.3 && <0.6, + adjunctions ==4.4.*, + vector-space ==0.13.*, + comonad >=5.0.3 && <5.1, + lens >=4.16.1 && <4.17, + ansi-terminal >=0.8.0.2 && <0.9 + default-language: Haskell2010 + ghc-options: -pgmL markdown-unlit diff --git a/src/SizedGrid.hs b/src/SizedGrid.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid.hs @@ -0,0 +1,22 @@ +{-# OPTIONS_GHC -fno-warn-unused-imports #-} + +module SizedGrid + ( + module X + -- * Rexported for generics-sop + , All + , SListI + , Compose + , I(..) + ) where + +import SizedGrid.Coord as X +import SizedGrid.Coord.Class as X +import SizedGrid.Coord.HardWrap as X +import SizedGrid.Coord.Periodic as X +import SizedGrid.Grid.Class as X +import SizedGrid.Grid.Focused as X +import SizedGrid.Grid.Grid as X +import SizedGrid.Ordinal as X + +import Generics.SOP diff --git a/src/SizedGrid/Coord.hs b/src/SizedGrid/Coord.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Coord.hs @@ -0,0 +1,226 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module SizedGrid.Coord where + +import SizedGrid.Coord.Class +import SizedGrid.Ordinal + +import Control.Applicative (liftA2) +import Control.Applicative (empty) +import Control.Lens ((^.)) +import Control.Monad.State +import Data.AdditiveGroup +import Data.Aeson +import Data.AffineSpace +import Data.Functor.Identity +import Data.List (intercalate) +import Data.Semigroup (Semigroup (..)) +import qualified Data.Vector as V +import Generics.SOP hiding (Generic, S, Z) +import qualified Generics.SOP as SOP +import GHC.Exts (Constraint) +import GHC.Generics (Generic) +import qualified GHC.TypeLits as GHC +import System.Random (Random (..)) + +-- | Length of a type level list +type family Length cs where + Length '[] = 0 + Length (c ': cs) = (GHC.+) 1 (Length cs) + +-- | A multideminsion coordinate +newtype Coord cs = Coord {unCoord :: NP I cs} + deriving (Generic) + +instance All Eq cs => Eq (Coord cs) where + Coord a == Coord b = + and $ + hcollapse $ hcliftA2 (Proxy :: Proxy Eq) (\(I x) (I y) -> K (x == y)) a b + +instance (All Eq cs, All Ord cs) => Ord (Coord cs) where + compare (Coord a) (Coord b) = + mconcat $ + hcollapse $ + hcliftA2 (Proxy :: Proxy Ord) (\(I x) (I y) -> K (compare x y)) a b + +instance All Show cs => Show (Coord cs) where + show (Coord a) = + "Coord [" ++ + intercalate + ", " + (hcollapse $ hcliftA (Proxy :: Proxy Show) (\(I x) -> K $ show x) a) ++ + "]" + +instance (All ToJSON cs) => ToJSON (Coord cs) where + toJSON (Coord a) = + Array $ + V.fromList $ + hcollapse $ hcmap (Proxy @ToJSON) (\(I x) -> K $ toJSON x) a + +instance All FromJSON cs => FromJSON (Coord cs) where + parseJSON = + withArray "Coord" $ \v -> + case SOP.fromList $ V.toList v of + Just a -> + Coord <$> + hsequence + (hcmap (Proxy @FromJSON) (\(K x) -> parseJSON x) a) + Nothing -> empty + + +instance All Semigroup cs => Semigroup (Coord cs) where + Coord a <> Coord b = Coord $ hcliftA2 (Proxy :: Proxy Semigroup) (liftA2 (<>)) a b + +instance (All Semigroup cs, All Monoid cs) => Monoid (Coord cs) where + mappend = (<>) + mempty = Coord $ hcpure (Proxy :: Proxy Monoid) (pure mempty) + +instance (All AdditiveGroup cs) => AdditiveGroup (Coord cs) where + zeroV = Coord $ hcpure (Proxy :: Proxy AdditiveGroup) (pure zeroV) + Coord a ^+^ Coord b = + Coord $ hcliftA2 (Proxy :: Proxy AdditiveGroup) (liftA2 (^+^)) a b + negateV (Coord a) = + Coord $ hcliftA (Proxy :: Proxy AdditiveGroup) (fmap negateV) a + Coord a ^-^ Coord b = + Coord $ hcliftA2 (Proxy :: Proxy AdditiveGroup) (liftA2 (^-^)) a b + +instance (All Random cs) => Random (Coord cs) where + random g = + let (c, g') = + runState + (hsequence $ hcpure (Proxy :: Proxy Random) (state random)) + g + in (Coord c, g') + randomR (Coord mi, Coord ma) g = + let (c, g') = + runState + (hsequence $ + hcliftA2 + (Proxy :: Proxy Random) + (\(I a) (I b) -> state (randomR (a, b))) + mi + ma) + g + in (Coord c, g') + +-- | The type of difference between two coords. A n-dimensional coord should have a `Diff` of an n-tuple of `Integers`. We use `Identity` and our 1-tuple. Unfortuantly, each instance is manual at the moment. +type family CoordDiff (cs :: [k]) :: * + +type instance CoordDiff '[] = () +type instance CoordDiff '[a] = Identity (Diff a) +type instance CoordDiff '[a, b] = (Diff a, Diff b) +type instance CoordDiff '[a, b, c] = (Diff a, Diff b, Diff c) +type instance CoordDiff '[a, b, c, d] = + (Diff a, Diff b, Diff c, Diff d) +type instance CoordDiff '[a, b, c, d, e] = + (Diff a, Diff b, Diff c, Diff d, Diff e) +type instance CoordDiff '[a, b, c, d, e, f] = + (Diff a, Diff b, Diff c, Diff d, Diff e, Diff f) + +-- | Apply `Diff` to each element of a type level list. This is required as type families can't be partially applied. +type family MapDiff xs where + MapDiff '[] = '[] + MapDiff (x ': xs) = Diff x ': MapDiff xs + +instance ( All AffineSpace cs + , AdditiveGroup (CoordDiff cs) + , IsProductType (CoordDiff cs) (MapDiff cs) + ) => + AffineSpace (Coord cs) where + type Diff (Coord cs) = CoordDiff cs + Coord a .-. Coord b = + let helper :: + All AffineSpace xs => NP I xs -> NP I xs -> NP I (MapDiff xs) + helper Nil Nil = Nil + helper (I x :* xs) (I y :* ys) = I (x .-. y) :* helper xs ys + in to $ SOP $ SOP.Z $ helper a b + Coord a .+^ b = + let helper :: All AffineSpace xs => NP I xs -> NP I (MapDiff xs) -> NP I xs + helper Nil Nil = Nil + helper (I x :* xs) (I y :* ys) = I (x .+^ y) :* helper xs ys + in case from b of + SOP (SOP.Z bs) -> Coord $ helper a bs + _ -> error "Error in adding Coord. Should be unreachable" + +-- | Generate all possible coords in order +allCoord :: + forall cs. (All IsCoord cs) + => [Coord cs] +allCoord = Coord <$> hsequence (hcpure (Proxy :: Proxy IsCoord) allCoordLike) + +-- | The number of elements a coord can have. This is equal to the product of the `CoordSized` of each element +type family MaxCoordSize (cs :: [k]) :: GHC.Nat where + MaxCoordSize '[] = 1 + MaxCoordSize (c ': cs) = (CoordSized c) GHC.* (MaxCoordSize cs) + +-- | Convert a `Coord` to its position in a vector +coordPosition :: (All IsCoord cs) => Coord cs -> Int +coordPosition (Coord a) = + let helper :: (All IsCoord xs) => NP I xs -> Integer + helper Nil = 0 + helper (I c :* (cs :: NP I ys)) = + ordinalToNum (c ^. asOrdinal) * sizeOfList cs + helper cs + sizeOfList :: All IsCoord xs => NP I xs -> Integer + sizeOfList = + product . + hcollapse . + hcmap + (Proxy :: Proxy IsCoord) + (\(I (_ :: a)) -> K $ 1 + maxCoordSize (Proxy :: Proxy a)) + in fromIntegral $ helper a + +-- | All Diffs of the members of the list must be equal +type family AllDiffSame a xs :: Constraint where + AllDiffSame _ '[] = () + AllDiffSame a (x ': xs) = (Diff x ~ a, AllDiffSame a xs) + +-- | Calculate the Moore neighbourhood around a point. Includes the center +moorePoints :: + forall a cs. (Enum a, Num a, AllDiffSame a cs, All AffineSpace cs) + => a + -> Coord cs + -> [Coord cs] +moorePoints n (Coord cs) = + let helper :: (All AffineSpace xs, AllDiffSame a xs) => NP I xs -> [NP I xs] + helper Nil = [Nil] + helper (I a :* as) = do + delta :: a <- [-n .. n] + next <- helper as + return (I (a .+^ delta) :* next) + in map Coord $ helper cs + +-- | Calculate the von Neuman neighbourhood around a point. Includes the center +vonNeumanPoints :: + forall a cs. + ( Enum a + , Num a + , Ord a + , All Integral (MapDiff cs) + , AllDiffSame a cs + , All AffineSpace cs + , Ord (CoordDiff cs) + , IsProductType (CoordDiff cs) (MapDiff cs) + , AdditiveGroup (CoordDiff cs) + ) + => a + -> Coord cs + -> [Coord cs] +vonNeumanPoints n c = + let helper :: Coord cs -> Bool + helper new = + sum + (hcollapse $ + hcmap + (Proxy :: Proxy Integral) + (\(I a) -> K (abs $ fromIntegral a)) $ + from (min (new .-. c) (c .-. new))) <= n + in filter helper $ moorePoints n c diff --git a/src/SizedGrid/Coord/Class.hs b/src/SizedGrid/Coord/Class.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Coord/Class.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module SizedGrid.Coord.Class where + +import SizedGrid.Ordinal + +import Control.Lens +import Data.Proxy +import GHC.TypeLits + +-- | Everything that can be uses as a Coordinate. The only required function is `asOrdinal` and the type instance of `CoordSized`: the rest can be derived automatically. +-- +-- This is kind * -> Constraint for ease of use later. There is some argument that it should be of kind (Nat -> *) -> Constraint and we can remove `CoordSized` +class (1 <= CoordSized c, KnownNat (CoordSized c)) => IsCoord c where + -- | The maximum number of values that a Coord can take + type CoordSized c :: Nat + -- | As each coord represents a finite number of states, it must be isomorphic to an Ordinal + asOrdinal :: Iso' c (Ordinal (CoordSized c)) + -- | The origin. If c is an instance of `Monoid`, this should be mempty + zeroPosition :: c + default zeroPosition :: Monoid c => c + zeroPosition = mempty + -- | Retrive a `Proxy` of the size + sCoordSized :: proxy c -> Proxy (CoordSized c) + sCoordSized _ = Proxy + -- | The largest possible number expressable + maxCoordSize :: proxy c -> Integer + maxCoordSize p = natVal (sCoordSized p) - 1 + +instance (1 <= n, KnownNat n) => IsCoord (Ordinal n) where + type CoordSized (Ordinal n) = n + asOrdinal = id + zeroPosition = Ordinal (Proxy @0) + +-- | Enumerate all possible values of a coord, in order +allCoordLike :: IsCoord c => [c] +allCoordLike = toListOf (traverse . re asOrdinal) [minBound .. maxBound] diff --git a/src/SizedGrid/Coord/HardWrap.hs b/src/SizedGrid/Coord/HardWrap.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Coord/HardWrap.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module SizedGrid.Coord.HardWrap where + +import SizedGrid.Coord.Class +import SizedGrid.Ordinal + +import Control.Lens (iso) +import Data.Aeson +import Data.AffineSpace +import Data.Maybe (fromJust) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (Semigroup (..)) +import GHC.TypeLits +import System.Random (Random (..)) + +-- | A coordinate that clamps its numbers +newtype HardWrap (n :: Nat) = HardWrap + { unHardWrap :: Ordinal n + } deriving (Eq,Show,Ord) + +deriving instance (KnownNat n, 1 <= n) => Random (HardWrap n) +deriving instance (KnownNat n, 1 <= n) => Enum (HardWrap n) +deriving instance (KnownNat n, 1 <= n) => Bounded (HardWrap n) +deriving instance KnownNat n => ToJSON (HardWrap n) +deriving instance KnownNat n => FromJSON (HardWrap n) +deriving instance KnownNat n => ToJSONKey (HardWrap n) +deriving instance KnownNat n => FromJSONKey (HardWrap n) + +instance (1 <= n, KnownNat n) => IsCoord (HardWrap n) where + type CoordSized (HardWrap n) = n + asOrdinal = iso unHardWrap HardWrap + +instance (1 <= n, KnownNat n) => Semigroup (HardWrap n) where + HardWrap a <> HardWrap b = + HardWrap $ + fromJust $ + numToOrdinal $ + min + (maxCoordSize (Proxy @(HardWrap n))) + (ordinalToNum a + ordinalToNum b) + +instance (KnownNat n, 1 <= n) => Monoid (HardWrap n) where + mempty = HardWrap minBound + mappend = (<>) + +instance (1 <= n, KnownNat n) => AffineSpace (HardWrap n) where + type Diff (HardWrap n) = Integer + HardWrap a .-. HardWrap b = + max 0 $ + min + (fromIntegral $ maxCoordSize (Proxy @(HardWrap n))) + (ordinalToNum a - ordinalToNum b) + HardWrap a .+^ b = HardWrap $ fromJust $ numToOrdinal $ + max 0 $ + min (maxCoordSize (Proxy @(HardWrap n))) $ + ((ordinalToNum a) + fromIntegral b) diff --git a/src/SizedGrid/Coord/Periodic.hs b/src/SizedGrid/Coord/Periodic.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Coord/Periodic.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module SizedGrid.Coord.Periodic where + +import SizedGrid.Coord.Class +import SizedGrid.Ordinal + +import Control.Lens +import Data.AdditiveGroup +import Data.Aeson +import Data.AffineSpace +import Data.Maybe (fromJust) +import Data.Proxy +import Data.Semigroup +import GHC.TypeLits +import System.Random + +-- | A coordinate with periodic boundaries, as if on a taurus +newtype Periodic (n :: Nat) = Periodic + { unPeriodic :: Ordinal n + } deriving (Eq, Show, Ord) + +deriving instance (1 <= n, KnownNat n) => Random (Periodic n) + +deriving instance KnownNat n => ToJSON (Periodic n) +deriving instance KnownNat n => ToJSONKey (Periodic n) +deriving instance KnownNat n => FromJSON (Periodic n) +deriving instance KnownNat n => FromJSONKey (Periodic n) + +instance (1 <= n, KnownNat n) => Enum (Periodic n) where + toEnum x = + Periodic $ + fromJust $ + numToOrdinal $ + (fromIntegral x) `mod` (maxCoordSize (Proxy @(Periodic n))) + fromEnum (Periodic o) = ordinalToNum o + +instance (1 <= n, KnownNat n) => IsCoord (Periodic n) where + type CoordSized (Periodic n) = n + asOrdinal = iso unPeriodic Periodic + +instance (1 <= n, KnownNat n) => Semigroup (Periodic n) where + Periodic a <> Periodic b = + let n = maxCoordSize (Proxy :: Proxy (Periodic n)) + 1 + in Periodic $ + fromJust $ numToOrdinal ((ordinalToNum a + ordinalToNum b) `mod` n) + +instance (1 <= n, KnownNat n) => Monoid (Periodic n) where + mappend = (<>) + mempty = Periodic minBound + +instance (1 <= n, KnownNat n) => AdditiveGroup (Periodic n) where + zeroV = mempty + (^+^) = (<>) + negateV (Periodic o) = + let n = maxCoordSize (Proxy @(Periodic n)) + 1 + in Periodic $ fromJust $ numToOrdinal (negate (ordinalToNum o) `mod` n) + +instance (1 <= n, KnownNat n) => AffineSpace (Periodic n) where + type Diff (Periodic n) = Integer + Periodic a .-. Periodic b = + (ordinalToNum a - ordinalToNum b) `mod` + (fromIntegral $ maxCoordSize (Proxy @(Periodic n)) + 1) + Periodic a .+^ b = + Periodic $ + fromJust $ + numToOrdinal $ + (ordinalToNum a + b) `mod` + (fromIntegral $ maxCoordSize (Proxy @(Periodic n)) + 1) diff --git a/src/SizedGrid/Grid/Class.hs b/src/SizedGrid/Grid/Class.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Grid/Class.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +module SizedGrid.Grid.Class where + +import SizedGrid.Coord +import SizedGrid.Coord.Class +import SizedGrid.Grid.Focused +import SizedGrid.Grid.Grid + +import Control.Lens hiding (index) +import Data.Functor.Rep +import Data.Semigroup hiding (All (..)) +import Generics.SOP +import qualified GHC.TypeLits as GHC + +-- | Conversion between `Grid` and `FocusedGrid` and access grids at a `Coord` +class IsGrid cs grid | grid -> cs where + -- | Get the element at a grid location. This is a lens because we know it must exist + gridIndex :: Coord cs -> Lens' (grid a) a + -- | Convert to, or run a function over, a `Grid` + asGrid :: Lens' (grid a) (Grid cs a) + -- | Convert to, or run a function over, a `FocusedGrid` + asFocusedGrid :: Lens' (grid a) (FocusedGrid cs a) + +instance ( GHC.KnownNat (MaxCoordSize cs) + , All Semigroup cs + , All Monoid cs + , All IsCoord cs + ) => + IsGrid cs (Grid cs) where + gridIndex coord = + lens + (\g -> index g coord) + (\(Grid v) a -> Grid (v & ix (coordPosition coord) .~ a)) + asGrid = id + asFocusedGrid = lens (\g -> FocusedGrid g mempty) (\_ fg -> focusedGrid fg) + +instance ( GHC.KnownNat (MaxCoordSize cs) + , All IsCoord cs + , All Monoid cs + , All Semigroup cs + ) => + IsGrid cs (FocusedGrid cs) where + gridIndex c = + (\f (FocusedGrid g p) -> (\g' -> FocusedGrid g' p) <$> f g) . + gridIndex c + asGrid = lens focusedGrid (\(FocusedGrid _ p) g -> FocusedGrid g p) + asFocusedGrid = id diff --git a/src/SizedGrid/Grid/Focused.hs b/src/SizedGrid/Grid/Focused.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Grid/Focused.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} + +module SizedGrid.Grid.Focused where + +import SizedGrid.Coord +import SizedGrid.Coord.Class +import SizedGrid.Grid.Grid + +import Control.Comonad +import Control.Comonad.Store +import Data.Functor.Rep +import Data.Semigroup (Semigroup (..)) +import Generics.SOP +import qualified GHC.TypeLits as GHC + +-- | Similar to `Grid`, but this has a focus on a certain square. Becuase of this we loose some instances, such as `Applicative`, but we gain a `Comonad` and `ComonadStore` instance. We can convert between a focused and unfocused list using facilites in `IsGrid` +data FocusedGrid cs a = FocusedGrid + { focusedGrid :: Grid cs a + , focusedGridPosition :: Coord cs + } deriving (Functor,Foldable,Traversable) + +instance ( GHC.KnownNat (MaxCoordSize cs) + , All IsCoord cs + , All Monoid cs + , All Semigroup cs + , SListI cs + ) => + Comonad (FocusedGrid cs) where + extract (FocusedGrid g p) = index g p + duplicate (FocusedGrid g p) = FocusedGrid (tabulate (FocusedGrid g)) p + +instance ( GHC.KnownNat (MaxCoordSize cs) + , All IsCoord cs + , All Monoid cs + , All Semigroup cs + , SListI cs + ) => + ComonadStore (Coord cs) (FocusedGrid cs) where + pos = focusedGridPosition + peek p (FocusedGrid g _) = index g p + peeks func (FocusedGrid g p) = index g (func p) + seek p (FocusedGrid g _) = FocusedGrid g p + seeks func (FocusedGrid g p) = FocusedGrid g $ func p diff --git a/src/SizedGrid/Grid/Grid.hs b/src/SizedGrid/Grid/Grid.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Grid/Grid.hs @@ -0,0 +1,140 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module SizedGrid.Grid.Grid where + +import SizedGrid.Coord +import SizedGrid.Coord.Class + +import Control.Lens hiding (index) +import Data.Aeson +import Data.Distributive +import Data.Functor.Classes +import Data.Functor.Rep +import Data.Proxy (Proxy (..)) +import qualified Data.Vector as V +import Generics.SOP +import GHC.Exts +import qualified GHC.TypeLits as GHC + +-- | A multi dimensional sized grid +newtype Grid (cs :: [*]) a = Grid + { unGrid :: V.Vector a + } deriving (Eq, Show, Functor, Foldable, Traversable, Eq1, Show1) + +instance GHC.KnownNat (MaxCoordSize cs) => Applicative (Grid cs) where + pure = + Grid . + V.replicate + (fromIntegral $ GHC.natVal (Proxy :: Proxy (MaxCoordSize cs))) + Grid fs <*> Grid as = Grid $ V.zipWith ($) fs as + +instance (GHC.KnownNat (MaxCoordSize cs), All IsCoord cs) => Monad (Grid cs) where + g >>= f = imap (\p a -> f a `index` p) g + +instance (GHC.KnownNat (MaxCoordSize cs), All IsCoord cs) => + Distributive (Grid cs) where + distribute = distributeRep + +instance (All IsCoord cs, GHC.KnownNat (MaxCoordSize cs)) => + Representable (Grid cs) where + type Rep (Grid cs) = Coord cs + tabulate func = Grid $ V.fromList $ map func $ allCoord + index (Grid v) c = v V.! coordPosition c + +instance (All IsCoord cs) => + FunctorWithIndex (Coord cs) (Grid cs) where + imap func (Grid v) = Grid $ V.zipWith func (V.fromList allCoord) v + +instance (All IsCoord cs) => + FoldableWithIndex (Coord cs) (Grid cs) where + ifoldMap func (Grid v) = foldMap id $ V.zipWith func (V.fromList allCoord) v + +instance (All IsCoord cs) => + TraversableWithIndex (Coord cs) (Grid cs) where + itraverse func (Grid v) = + Grid <$> sequenceA (V.zipWith func (V.fromList allCoord) v) + +-- | The first element of a type level list +type family Head xs where + Head (x ': xs) = x + +-- | All but the first elements of a type level list +type family Tail xs where + Tail (x ': xs) = xs + +-- | Given a grid type, give back a series of nested lists repesenting the grid. The lists will have a number of layers equal to the dimensionality. +type family CollapseGrid cs a where + CollapseGrid '[] a = a + CollapseGrid (c ': cs) a = [CollapseGrid cs a] + +-- | A Constraint that all grid sizes are instances of `KnownNat` +type family AllGridSizeKnown cs :: Constraint where + AllGridSizeKnown '[] = () + AllGridSizeKnown cs = ( GHC.KnownNat (CoordSized (Head cs)) + , GHC.KnownNat (MaxCoordSize (Tail cs)) + , AllGridSizeKnown (Tail cs)) + +-- | Convert a vector into a list of `Vector`s, where all the elements of the list have the given size. +splitVectorBySize :: Int -> V.Vector a -> [V.Vector a] +splitVectorBySize n v + | V.length v >= n = V.take n v : splitVectorBySize n (V.drop n v) + | V.null v = [] + | otherwise = [v] + +-- | Convert a grid to a series of nested lists. This removes type level information, but it is sometimes easier to work with lists +collapseGrid :: + forall cs a. + ( SListI cs + , AllGridSizeKnown cs + ) + => Grid cs a + -> CollapseGrid cs a +collapseGrid (Grid v) = + case (shape :: Shape cs) of + ShapeNil -> v V.! 0 + ShapeCons _ -> + map (collapseGrid . Grid @(Tail cs)) $ + splitVectorBySize + (fromIntegral $ GHC.natVal (Proxy @(MaxCoordSize (Tail cs)))) + v + +-- | Convert a series of nested lists to a grid. If the size of the grid does not match the size of lists this will be `Nothing` +gridFromList :: + forall cs a. (SListI cs, AllGridSizeKnown cs) + => CollapseGrid cs a + -> Maybe (Grid cs a) +gridFromList cg = + case (shape :: Shape cs) of + ShapeNil -> Just $ Grid $ V.singleton $ cg + ShapeCons _ -> + if length cg == fromIntegral (GHC.natVal (Proxy @(CoordSized (Head cs)))) + then Grid . mconcat <$> + traverse (fmap unGrid . gridFromList @(Tail cs)) cg + else Nothing + +instance (AllGridSizeKnown cs, ToJSON a, SListI cs) => ToJSON (Grid cs a) where + toJSON (Grid v) = + case (shape :: Shape cs) of + ShapeNil -> toJSON (v V.! 0) + ShapeCons _ -> + toJSON $ + map (toJSON . Grid @(Tail cs)) $ + splitVectorBySize + (fromIntegral $ GHC.natVal (Proxy @(MaxCoordSize (Tail cs)))) + v + +instance (All IsCoord cs, FromJSON a) => FromJSON (Grid cs a) where + parseJSON v = case (shape :: Shape cs) of + ShapeNil -> Grid . V.singleton <$> parseJSON v + ShapeCons _ -> do + a :: [Grid (Tail cs) a] <- parseJSON v + return $ Grid $ foldMap unGrid a diff --git a/src/SizedGrid/Internal/Type.hs b/src/SizedGrid/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Internal/Type.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +-- | +-- Module : SizedGrid.Internal.Type +-- Copyright : (C) 2018-18 Edward Wastell +-- License : MIT -style (see the file LICENSE) +-- Maintainer : Edward Wastell +-- Stability : provisional + +module SizedGrid.Internal.Type where + +import Data.Constraint +import Data.Proxy +import GHC.TypeLits +import Unsafe.Coerce + +-- | A singleton type for Bools +data SBool a where + STrue :: SBool 'True + SFalse :: SBool 'False + +deriving instance Show (SBool a) + +-- | A type constraint for getting `SingI` +class SBoolI a where + sBool :: SBool a + +instance SBoolI 'True where + sBool = STrue + +instance SBoolI 'False where + sBool = SFalse + +-- | Give a runtime representation of a type level number being less than or equal than another +sLessThan :: + forall n m. (KnownNat n, KnownNat m) + => Proxy n + -> Proxy m + -> SBool (n <=? m) +sLessThan _ _ = + if natVal (Proxy @n) <= natVal (Proxy @m) + then unsafeCoerce STrue + else unsafeCoerce SFalse + +-- | A Dict prove that m - 1 + 1 is m +takeAddIsId :: forall m . Dict (((m - 1) + 1) ~ m) +takeAddIsId = unsafeCoerce (Dict :: Dict (a ~ a)) + +-- | Magic is stole from Constraints, and I don't really understand it, but it is needed for 'takeNat' +newtype Magic n = Magic (KnownNat n => Dict (KnownNat n)) + +-- | Also don't understand +magic :: + forall n m o. + (Integer -> Integer -> Integer) + -> (KnownNat n, KnownNat m) :- KnownNat o +magic f = + Sub $ + unsafeCoerce + (Magic Dict) + (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m)) + +-- | Runtime proof that n - m is an insance of KnownNat if n and m are +takeNat :: (KnownNat n, KnownNat m) :- KnownNat (n - m) +takeNat = magic (-) diff --git a/src/SizedGrid/Ordinal.hs b/src/SizedGrid/Ordinal.hs new file mode 100644 --- /dev/null +++ b/src/SizedGrid/Ordinal.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module SizedGrid.Ordinal where + +import SizedGrid.Internal.Type + +import Control.Monad (guard) +import Data.Aeson +import Data.Constraint +import Data.Constraint.Nat +import Data.Maybe (fromJust) +import Data.Proxy +import GHC.TypeLits +import System.Random + +-- | An Ordinal can only hold m different values, ususally corresponding to 0 .. m - 1. We store it here using a `Proxy` of a type level number and use constraints to keep the required invariants. +-- +-- Desprite represeting a number, Ordinal is not an instance of Num and many functions (such as negate) would only be partial +data Ordinal m where + Ordinal :: (KnownNat n, KnownNat m, (n + 1 <=? m) ~ 'True ) => Proxy n -> Ordinal m + +instance Show (Ordinal m) where + show (Ordinal p) = "Ordinal (" ++ show (natVal p) ++ "/" ++ show (natVal (Proxy @m)) ++ ")" + +instance Eq (Ordinal m) where + Ordinal a == Ordinal b = natVal a == natVal b + +instance Ord (Ordinal m) where + compare (Ordinal a) (Ordinal b) = compare (natVal a) (natVal b) + +instance (1 <= m, KnownNat m) => Random (Ordinal m) where + randomR (mi, ma) g = + let (n, g') = randomR (fromEnum mi, fromEnum ma) g + in (toEnum n, g') + random = randomR (minBound, maxBound) + +-- | Convert a normal integral to an ordinal. If it is outside the range (< 0 or >= m), Nothing is returned. +numToOrdinal :: + forall a m. (KnownNat m, Integral a) + => a + -> Maybe (Ordinal m) +numToOrdinal n = + case someNatVal (fromIntegral n) of + Nothing -> Nothing + Just (SomeNat (p :: Proxy n)) -> + (case sLessThan (Proxy @ (n + 1)) (Proxy :: Proxy m) of + SFalse -> Nothing + STrue -> Just $ Ordinal p) \\ plusNat @n @1 + +-- | Transform an ordinal to a given number +ordinalToNum :: Num a => Ordinal m -> a +ordinalToNum (Ordinal p) = fromIntegral $ natVal p + +instance (1 <= m, KnownNat m) => Bounded (Ordinal m) where + minBound = Ordinal (Proxy @0) + maxBound = + Ordinal (Proxy @(m - 1)) \\ + (eqLe @((m - 1) + 1) @m `trans` Sub @() takeAddIsId) \\ + takeNat @m @1 + +instance (1 <= m, KnownNat m) => Enum (Ordinal m) where + toEnum = fromJust . numToOrdinal + fromEnum (Ordinal p) = fromIntegral $ natVal p + +instance KnownNat m => ToJSON (Ordinal m) where + toJSON (Ordinal p) = object ["size" .= natVal (Proxy @m), "value" .= natVal p] + +instance KnownNat m => FromJSON (Ordinal m) where + parseJSON = withObject "Ordinal" $ \v -> do + size <- v .: "size" + guard (size == natVal (Proxy @m)) + Just o <- numToOrdinal @Integer <$> v .: "value" + return o + +instance KnownNat m => ToJSONKey (Ordinal m) +instance KnownNat m => FromJSONKey (Ordinal m) diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,140 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module Main where + +import SizedGrid.Coord +import SizedGrid.Coord.Class +import SizedGrid.Coord.HardWrap +import SizedGrid.Coord.Periodic +import SizedGrid.Grid.Grid + +import Test.Utils + +import Control.Monad (replicateM) +import Data.Functor.Rep +import Data.Proxy +import Generics.SOP hiding (S, Z) +import GHC.TypeLits +import qualified GHC.TypeLits as GHC +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import Test.Tasty +import Test.Tasty.Hedgehog +import Test.Tasty.HUnit + +assertOrderd :: Ord a => [a] -> Assertion +assertOrderd = + let helper [] = True + helper (x:xs) = all (x <=) xs && helper xs + in assertBool "Ordered" . helper + +testAllCoordOrdered :: + forall cs proxy. (All Eq cs, All Ord cs, All IsCoord cs) + => proxy (Coord cs) + -> TestTree +testAllCoordOrdered _ = + testCase "allCoord is ordered" $ assertOrderd (allCoord @cs) + +genPeriodic :: (1 <= n, GHC.KnownNat n) => Gen (Periodic n) +genPeriodic = Periodic <$> Gen.enumBounded + +genCoord :: SListI cs => NP Gen cs -> Gen (Coord cs) +genCoord start = Coord <$> hsequence start + +gridTests :: + forall cs a x y. + ( Show (Coord cs) + , Eq (Coord cs) + , All IsCoord cs + , GHC.KnownNat (MaxCoordSize cs) + , Show a + , Eq a + , AllGridSizeKnown cs + , cs ~ '[x,y] + ) + => Gen (Coord cs) + -> Gen a + -> [TestTree] +gridTests genC genA = + let tabulateIndex = + property $ do + c <- forAll genC + c === index (tabulate id :: Grid cs (Coord cs)) c + collapseUnCollapse = + property $ do + g :: Grid cs a <- forAll (sequenceA $ pure genA) + Just g === gridFromList (collapseGrid g) + uncollapseCollapse = + property $ do + cg :: [[a]] <- + replicateM (fromIntegral $ natVal (Proxy @(CoordSized x))) $ + replicateM (fromIntegral $ natVal (Proxy @(CoordSized y))) $ forAll genA + Just cg === (collapseGrid <$> gridFromList @cs cg) + in [ testProperty "Tabulate index" tabulateIndex + , testProperty "Collapse UnCollapse" collapseUnCollapse + , testProperty "UnCollapse and Collapse" uncollapseCollapse + ] + +main :: IO () +main = + let periodic = + let g :: Gen (Periodic 10) = genPeriodic + in [ semigroupLaws g + , monoidLaws g + , additiveGroupLaws g + , affineSpaceLaws g + , aesonLaws g + ] + hardWrap = + let g :: Gen (HardWrap 10) = HardWrap <$> Gen.enumBounded + in [semigroupLaws g, monoidLaws g, affineSpaceLaws g, aesonLaws g] + coord = + let g :: Gen (Coord '[ HardWrap 10, Periodic 20]) = + genCoord + ((HardWrap <$> Gen.enumBounded) :* + (Periodic <$> Gen.enumBounded) :* + Nil) + in [semigroupLaws g, monoidLaws g, affineSpaceLaws g, aesonLaws g, testAllCoordOrdered g] + coord2 = + let g :: Gen (Coord '[ Periodic 10, Periodic 20]) = + genCoord + ((Periodic <$> Gen.enumBounded) :* + (Periodic <$> Gen.enumBounded) :* + Nil) + in [ semigroupLaws g + , monoidLaws g + , affineSpaceLaws g + , additiveGroupLaws g + , aesonLaws g + , testAllCoordOrdered g + ] + in defaultMain $ + testGroup + "tests" + [ testGroup "Periodic 20" periodic + , testGroup "HardWrap 20" hardWrap + , testGroup "Coord [HardWrap 10, Periodic 20]" coord + , testGroup "Coord [Periodic 10, Periodic 20]" coord2 + , testGroup + "Grid" + ((gridTests @'[ Periodic 10, Periodic 11] + (genCoord $ + (Periodic <$> Gen.enumBounded) :* + (Periodic <$> Gen.enumBounded) :* + Nil)) (Gen.int $ Range.linear 0 100) ++ + [ applicativeLaws + (Proxy @(Grid '[ Periodic 10, Periodic 11])) + (Gen.int $ Range.linear 0 100) + , aesonLaws (sequenceA $ pure @(Grid '[Periodic 10, Periodic 11] ) $ + Gen.int $ Range.linear 0 100) + , eq1Laws (Proxy @(Grid '[Periodic 10, Periodic 20])) + ]) + ] diff --git a/tests/Test/Utils.hs b/tests/Test/Utils.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Utils.hs @@ -0,0 +1,136 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +module Test.Utils where + +import Data.AdditiveGroup +import Data.Aeson +import Data.AffineSpace +import Data.Functor.Classes +import Data.Proxy +import Data.Semigroup +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import Test.Tasty +import Test.Tasty.Hedgehog +import Test.Tasty.HUnit + +eq1Laws :: + forall f. (Eq1 f, Applicative f) + => Proxy f + -> TestTree +eq1Laws _ = + let nilEq = + assertEqual "Nil equal" True $ liftEq (==) (pure ()) (pure @f ()) + in testGroup "Eq1 Laws" [testCase "Nil Eq" nilEq] + +aesonLaws :: (Show a, Eq a, ToJSON a, FromJSON a) => Gen a -> TestTree +aesonLaws gen = + let encodeDecode = property $ do + a <- forAll gen + Just a === decode (encode a) + in testGroup "Aeson Laws" [testProperty "Encode decode" encodeDecode] + +semigroupLaws :: (Show a, Eq a, Semigroup a) => Gen a -> TestTree +semigroupLaws gen = + let assoc = property $ do + a <- forAll gen + b <- forAll gen + c <- forAll gen + a <> (b <> c) === (a <> b) <> c + in testGroup "Semigroup Laws" [testProperty "Associative" assoc] + +monoidLaws :: (Show a, Eq a, Monoid a) => Gen a -> TestTree +monoidLaws gen = + let assoc = + property $ do + a <- forAll gen + b <- forAll gen + c <- forAll gen + mappend a (mappend b c) === mappend (mappend a b) c + memptyId = + property $ do + a <- forAll gen + a === mappend mempty a + a === mappend a mempty + concatIsFold = + property $ do + as <- forAll $ Gen.list (Range.linear 0 100) gen + mconcat as === foldr mappend mempty as + in testGroup + "Monoid laws" + [ testProperty "Associative" assoc + , testProperty "Mempty Id" memptyId + , testProperty "Concat is Fold" concatIsFold + ] + +additiveGroupLaws :: (Show a, Eq a, AdditiveGroup a) => Gen a -> TestTree +additiveGroupLaws gen = + let assoc = + property $ do + a <- forAll gen + b <- forAll gen + c <- forAll gen + a ^+^ (b ^+^ c) === (a ^+^ b) ^+^ c + zeroId = + property $ do + a <- forAll gen + a === zeroV ^+^ a + a === a ^+^ zeroV + inverseId = property $ do + a <- forAll gen + a ^-^ a === zeroV + takeLeaves = property $ do + a <- forAll gen + b <- forAll gen + a ^-^ (a ^-^ b) === b + in testGroup + "AdditiveGroup laws" + [ testProperty "Associative" assoc + , testProperty "Zero Id" zeroId + , testProperty "Inverse id is zeroV" inverseId + , testProperty "a - (a - b) = b" takeLeaves + ] + +affineSpaceLaws :: + (Show a, Eq a, AffineSpace a, Eq (Diff a), Show (Diff a)) + => Gen a + -> TestTree +affineSpaceLaws gen = + let addZero = + property $ do + a <- forAll gen + a === a .+^ zeroV + takeSelf = + property $ do + a <- forAll gen + a .-. a === zeroV + in testGroup + "AffineSpace Laws" + [testProperty "Add Zero" addZero, testProperty "Take self" takeSelf] + +applicativeLaws :: + forall f a. + (Applicative f, Traversable f, Show (f a), Eq (f a), Num a, Show a) + => Proxy f + -> Gen a + -> TestTree +applicativeLaws _ gen = + let genF :: Gen (f a) = sequence $ pure gen + identiy = + property $ do + v <- forAll genF + v === (pure id <*> v) + homomorphism = + property $ do + x <- forAll gen + f <- (+) <$> forAll gen + (pure f <*> pure x) === pure @f (f x) + in testGroup + "Applicative Laws" + [ testProperty "Identity" identiy + , testProperty "Homomorphism" homomorphism + ]