Safe Haskell	None
Language	Haskell2010

SizedGrid.Ordinal

Synopsis

data Ordinal m where
- Ordinal :: (KnownNat n, KnownNat m, ((n + 1) <=? m) ~ True) => Proxy n -> Ordinal m
numToOrdinal :: forall a m. (KnownNat m, Integral a) => a -> Maybe (Ordinal m)
ordinalToNum :: Num a => Ordinal m -> a
strengthenOrdinal :: forall n m. (KnownNat m, n <= m) => Ordinal n -> Ordinal m
weakenOrdinal :: KnownNat m => Ordinal n -> Maybe (Ordinal m)
_Ordinal :: (KnownNat n, Integral a) => Prism' a (Ordinal n)

Documentation

data Ordinal m where Source #

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

Constructors

Ordinal :: (KnownNat n, KnownNat m, ((n + 1) <=? m) ~ True) => Proxy n -> Ordinal m

Instances

(1 <= m, KnownNat m) => Bounded (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods minBound :: Ordinal m # maxBound :: Ordinal m #
(1 <= m, KnownNat m) => Enum (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods succ :: Ordinal m -> Ordinal m # pred :: Ordinal m -> Ordinal m # toEnum :: Int -> Ordinal m # fromEnum :: Ordinal m -> Int # enumFrom :: Ordinal m -> [Ordinal m] # enumFromThen :: Ordinal m -> Ordinal m -> [Ordinal m] # enumFromTo :: Ordinal m -> Ordinal m -> [Ordinal m] # enumFromThenTo :: Ordinal m -> Ordinal m -> Ordinal m -> [Ordinal m] #
Eq (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods (==) :: Ordinal m -> Ordinal m -> Bool # (/=) :: Ordinal m -> Ordinal m -> Bool #
Ord (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods compare :: Ordinal m -> Ordinal m -> Ordering # (<) :: Ordinal m -> Ordinal m -> Bool # (<=) :: Ordinal m -> Ordinal m -> Bool # (>) :: Ordinal m -> Ordinal m -> Bool # (>=) :: Ordinal m -> Ordinal m -> Bool # max :: Ordinal m -> Ordinal m -> Ordinal m # min :: Ordinal m -> Ordinal m -> Ordinal m #
Show (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods showsPrec :: Int -> Ordinal m -> ShowS # show :: Ordinal m -> String # showList :: [Ordinal m] -> ShowS #
KnownNat m => ToJSON (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods toJSON :: Ordinal m -> Value # toEncoding :: Ordinal m -> Encoding # toJSONList :: [Ordinal m] -> Value # toEncodingList :: [Ordinal m] -> Encoding #
KnownNat m => ToJSONKey (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods toJSONKey :: ToJSONKeyFunction (Ordinal m) # toJSONKeyList :: ToJSONKeyFunction [Ordinal m] #
KnownNat m => FromJSON (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods parseJSON :: Value -> Parser (Ordinal m) # parseJSONList :: Value -> Parser [Ordinal m] #
KnownNat m => FromJSONKey (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods fromJSONKey :: FromJSONKeyFunction (Ordinal m) # fromJSONKeyList :: FromJSONKeyFunction [Ordinal m] #
(1 <= m, KnownNat m) => Random (Ordinal m) Source #
Instance details Defined in SizedGrid.Ordinal Methods randomR :: RandomGen g => (Ordinal m, Ordinal m) -> g -> (Ordinal m, g) # random :: RandomGen g => g -> (Ordinal m, g) # randomRs :: RandomGen g => (Ordinal m, Ordinal m) -> g -> [Ordinal m] # randoms :: RandomGen g => g -> [Ordinal m] # randomRIO :: (Ordinal m, Ordinal m) -> IO (Ordinal m) # randomIO :: IO (Ordinal m) #
(1 <= n, KnownNat n) => IsCoord (Ordinal n) Source #
Instance details Defined in SizedGrid.Coord.Class Associated Types type CoordSized (Ordinal n) :: Nat Source # type CoordFromNat (Ordinal n) :: Nat -> Type Source # Methods asOrdinal :: Iso' (Ordinal n) (Ordinal (CoordSized (Ordinal n))) Source # zeroPosition :: Ordinal n Source # sCoordSized :: proxy (Ordinal n) -> Proxy (CoordSized (Ordinal n)) Source # maxCoordSize :: proxy (Ordinal n) -> Integer Source # maxCoord :: Ordinal n Source # asSizeProxy :: Ordinal n -> (forall (n0 :: Nat). (KnownNat n0, (n0 + 1) <= CoordSized (Ordinal n)) => Proxy n0 -> x) -> x Source # weakenIsCoord :: IsCoord (CoordFromNat (Ordinal n) n0) => Ordinal n -> Maybe (CoordFromNat (Ordinal n) n0) Source # strengthenIsCoord :: (IsCoord (CoordFromNat (Ordinal n) n0), CoordSized (Ordinal n) <= CoordSized (CoordFromNat (Ordinal n) n0)) => Ordinal n -> CoordFromNat (Ordinal n) n0 Source #
type CoordSized (Ordinal n) Source #
Instance details Defined in SizedGrid.Coord.Class type CoordSized (Ordinal n) = n
type CoordFromNat (Ordinal n) Source #
Instance details Defined in SizedGrid.Coord.Class type CoordFromNat (Ordinal n) = Ordinal

numToOrdinal :: forall a m. (KnownNat m, Integral a) => a -> Maybe (Ordinal m) Source #

Convert a normal integral to an ordinal. If it is outside the range (or= m), Nothing is returned.

ordinalToNum :: Num a => Ordinal m -> a Source #

Transform an ordinal to a given number

strengthenOrdinal :: forall n m. (KnownNat m, n <= m) => Ordinal n -> Ordinal m Source #

weakenOrdinal :: KnownNat m => Ordinal n -> Maybe (Ordinal m) Source #

_Ordinal :: (KnownNat n, Integral a) => Prism' a (Ordinal n) Source #

Convert between an ordinal and a usual number. This is a Prism as it may fail as Oridnals can only exist in a certain range.