Safe Haskell	None
Language	Haskell2010

Closed.Internal

Synopsis

newtype Closed (n :: Nat) (m :: Nat) = Closed {
- getClosed :: Integer
}
data Endpoint
- = Inclusive Nat
- | Exclusive Nat
type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: * where ...
type Single (n :: Nat) = Bounds (Inclusive n) (Inclusive n)
type FiniteNat (rhs :: Endpoint) = Bounds (Inclusive 0) rhs
lowerBound :: Closed n m -> Proxy n
upperBound :: Closed n m -> Proxy m
closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)
unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m
unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String
natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m
weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k
weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m
strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)
strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)
equals :: Closed n m -> Closed o p -> Bool
cmp :: Closed n m -> Closed o p -> Ordering
add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)
sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)
isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool

Documentation

newtype Closed (n :: Nat) (m :: Nat) #

Constructors

Closed
Fields getClosed :: Integer

Instances

(n <= m, KnownNat n, KnownNat m) => Bounded (Closed n m) #	Generate the lowest and highest inhabitant of a given `Closed` type
Instance details Defined in Closed.Internal 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
Instance details Defined in Closed.Internal 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
Instance details Defined in Closed.Internal 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) #
Instance details Defined in Closed.Internal 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
Instance details Defined in Closed.Internal 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
Instance details Defined in Closed.Internal 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) #
Instance details Defined in Closed.Internal Methods toRational :: Closed n m -> Rational #
Show (Closed n m) #
Instance details Defined in Closed.Internal Methods showsPrec :: Int -> Closed n m -> ShowS # show :: Closed n m -> String # showList :: [Closed n m] -> ShowS #
Generic (Closed n m) #
Instance details Defined in Closed.Internal 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) #
Instance details Defined in Closed.Internal Methods arbitrary :: Gen (Closed n m) # shrink :: Closed n m -> [Closed n m] #
Hashable (Closed n m) #
Instance details Defined in Closed.Internal Methods hashWithSalt :: Int -> Closed n m -> Int # hash :: Closed n m -> Int #
ToJSON (Closed n m) #
Instance details Defined in Closed.Internal Methods toJSON :: Closed n m -> Value # toEncoding :: Closed n m -> Encoding # toJSONList :: [Closed n m] -> Value # toEncodingList :: [Closed n m] -> Encoding #
(n <= m, KnownNat n, KnownNat m) => FromJSON (Closed n m) #
Instance details Defined in Closed.Internal Methods parseJSON :: Value -> Parser (Closed n m) # parseJSONList :: Value -> Parser [Closed n m] #
(n <= m, KnownNat n, KnownNat m) => FromField (Closed n m) #
Instance details Defined in Closed.Internal Methods parseField :: Field -> Parser (Closed n m) #
ToField (Closed n m) #
Instance details Defined in Closed.Internal Methods toField :: Closed n m -> Field #
NFData (Closed n m) #
Instance details Defined in Closed.Internal Methods rnf :: Closed n m -> () #
(n <= m, KnownNat n, KnownNat m) => PersistFieldSql (Closed n m) #
Instance details Defined in Closed.Internal Methods sqlType :: Proxy (Closed n m) -> SqlType #
(n <= m, KnownNat n, KnownNat m) => PersistField (Closed n m) #
Instance details Defined in Closed.Internal Methods toPersistValue :: Closed n m -> PersistValue # fromPersistValue :: PersistValue -> Either Text (Closed n m) #
type Rep (Closed n m) #
Instance details Defined in Closed.Internal type Rep (Closed n m) = D1 (MetaData "Closed" "Closed.Internal" "closed-0.2.0-3ymVSz7LxmA2YI4r8wx9Ji" True) (C1 (MetaCons "Closed" PrefixI True) (S1 (MetaSel (Just "getClosed") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)))

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

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

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

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

unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String #

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

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

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