Closed

Documentation

data Endpoint

Describe whether the endpoint of a Bounds includes or excludes its argument

Constructors

Inclusive Nat

Endpoint includes its argument

Exclusive Nat

Endpoint excludes its argument

data Closed (n :: Nat) (m :: Nat)

Instances

((<=) n m, KnownNat n, KnownNat m) => Bounded (Closed n m)

Generate the lowest and highest inhabitant of a given Closed type

Methods

minBound :: Closed n m

maxBound :: Closed n m

((<=) n m, KnownNat n, KnownNat m) => Enum (Closed n m)

Enumerate values in the range of a given Closed type

Methods

succ :: Closed n m -> Closed n m

pred :: Closed n m -> Closed n m

toEnum :: Int -> Closed n m

fromEnum :: Closed n m -> Int

enumFrom :: Closed n m -> [Closed n m]

enumFromThen :: Closed n m -> Closed n m -> [Closed n m]

enumFromTo :: Closed n m -> Closed n m -> [Closed n m]

enumFromThenTo :: Closed n m -> Closed n m -> Closed n m -> [Closed n m]

Eq (Closed n m)

Test equality on Closed values in the same range

Methods

(==) :: Closed n m -> Closed n m -> Bool

(/=) :: Closed n m -> Closed n m -> Bool

((<=) n m, KnownNat n, KnownNat m) => Integral (Closed n m)

Methods

quot :: Closed n m -> Closed n m -> Closed n m

rem :: Closed n m -> Closed n m -> Closed n m

div :: Closed n m -> Closed n m -> Closed n m

mod :: Closed n m -> Closed n m -> Closed n m

quotRem :: Closed n m -> Closed n m -> (Closed n m, Closed n m)

divMod :: Closed n m -> Closed n m -> (Closed n m, Closed n m)

toInteger :: Closed n m -> Integer

((<=) n m, KnownNat n, KnownNat m) => Num (Closed n m)

Bounded arithmetic, e.g. maxBound + 1 == maxBound

Methods

(+) :: Closed n m -> Closed n m -> Closed n m

(-) :: Closed n m -> Closed n m -> Closed n m

(*) :: Closed n m -> Closed n m -> Closed n m

negate :: Closed n m -> Closed n m

abs :: Closed n m -> Closed n m

signum :: Closed n m -> Closed n m

fromInteger :: Integer -> Closed n m

Ord (Closed n m)

Compare Closed values in the same range

Methods

compare :: Closed n m -> Closed n m -> Ordering

(<) :: Closed n m -> Closed n m -> Bool

(<=) :: Closed n m -> Closed n m -> Bool

(>) :: Closed n m -> Closed n m -> Bool

(>=) :: Closed n m -> Closed n m -> Bool

max :: Closed n m -> Closed n m -> Closed n m

min :: Closed n m -> Closed n m -> Closed n m

((<=) n m, KnownNat n, KnownNat m) => Real (Closed n m)

Methods

toRational :: Closed n m -> Rational

Show (Closed n m)

Methods

showsPrec :: Int -> Closed n m -> ShowS

show :: Closed n m -> String

showList :: [Closed n m] -> ShowS

Generic (Closed n m)

Associated Types

type Rep (Closed n m) :: * -> *

Methods

from :: Closed n m -> Rep (Closed n m) x

to :: Rep (Closed n m) x -> Closed n m

((<=) n m, KnownNat n, KnownNat m) => Arbitrary (Closed n m)

Methods

arbitrary :: Gen (Closed n m)

shrink :: Closed n m -> [Closed n m]

ToJSON (Closed n m)

Methods

toJSON :: Closed n m -> Value

toEncoding :: Closed n m -> Encoding

((<=) n m, KnownNat n, KnownNat m) => FromJSON (Closed n m)

Methods

parseJSON :: Value -> Parser (Closed n m)

((<=) n m, KnownNat n, KnownNat m) => FromField (Closed n m)

Methods

parseField :: Field -> Parser (Closed n m)

ToField (Closed n m)

Methods

toField :: Closed n m -> Field

NFData (Closed n m)

Methods

rnf :: Closed n m -> ()

Hashable (Closed n m)

Methods

hashWithSalt :: Int -> Closed n m -> Int

hash :: Closed n m -> Int

((<=) n m, KnownNat n, KnownNat m) => PersistFieldSql (Closed n m)

Methods

sqlType :: Proxy * (Closed n m) -> SqlType

((<=) n m, KnownNat n, KnownNat m) => PersistField (Closed n m)

Methods

toPersistValue :: Closed n m -> PersistValue

fromPersistValue :: PersistValue -> Either Text (Closed n m)

type Rep (Closed n m)

type Rep (Closed n m) = D1 * (MetaData "Closed" "Closed.Internal" "closed-0.2.0-HfHoG39kc4gDbpe37xN1Bs" True) (C1 * (MetaCons "Closed" PrefixI True) (S1 * (MetaSel (Just Symbol "getClosed") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Integer)))

type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: * where ...

Syntactic sugar to express open and half-open intervals using the Closed type

Equations

Bounds (Inclusive n) (Inclusive m) = Closed n m

Bounds (Inclusive n) (Exclusive m) = Closed n (m - 1)

Bounds (Exclusive n) (Inclusive m) = Closed (n + 1) m

Bounds (Exclusive n) (Exclusive m) = Closed (n + 1) (m - 1)

type Single (n :: Nat) = Bounds (Inclusive n) (Inclusive n)

Syntactic sugar to express a value that has only one non-bottom inhabitant using the Closed type

type FiniteNat (rhs :: Endpoint) = Bounds (Inclusive 0) rhs

Syntactic sugar to express a value whose lower bound is zero

closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)

Safely create a Closed value using the specified argument

unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m

Create a Closed value throwing an error if the argument is not in range

getClosed :: Closed n m -> Integer

lowerBound :: Closed n m -> Proxy n

Proxy for the lower bound of a Closed value

upperBound :: Closed n m -> Proxy m

Proxy for the upper bound of a Closed value

equals :: Closed n m -> Closed o p -> Bool infix 4

Test two different types of Closed values for equality.

cmp :: Closed n m -> Closed o p -> Ordering

Compare two different types of Closed values

natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m

Convert a type-level literal into a Closed value

weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k

Add inhabitants at the end

weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m

Add inhabitants at the beginning

strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)

Remove inhabitants from the end. Returns Nothing if the input was removed

strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)

Remove inhabitants from the beginning. Returns Nothing if the input was removed

add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)

Add two different types of Closed values

sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))

Subtract two different types of Closed values Returns Left for negative results, and Right for positive results.

multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)

Multiply two different types of Closed values

isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool

Verifies that a given Closed value is valid. Should always return True unles you bring the Closed.Internal.Closed constructor into scope, or use unsafeCoerce or other nasty hacks