-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Haskell interval types. Bounds checking.
--
-- Haskell interval types. Bounds checking.
@package i
@version 0.1
-- | I am a Haskell module designed to be imported as follows:
--
--
-- import I (I)
-- import I qualified
--
--
-- I exist so that you don't have to manually check that a value
-- is within an interval. For example:
--
--
module I
-- | A value of type x known to be within the interval
-- determined by the left end l and right end r.
data I (x :: Type) (l :: L x) (r :: R x)
-- | The kind of the type-level representation of x in
-- I x l r, as it appears in Known x l r
-- t.
type family T (x :: Type) :: k
-- | Type-level verison of minBound :: x. If
-- x is unbounded on the left end, then it's ok to leave
-- MinT x undefined. If defined, it should match what
-- MinL means.
type family MinT (x :: Type) :: T x
-- | Type-level verison of maxBound :: x. If
-- x is unbounded on the right end, then it's ok to leave
-- MaxT x undefined. If defined, it should match what
-- MaxR means.
type family MaxT (x :: Type) :: T x
-- | The kind of l in I x l r.
type family L (x :: Type) :: k
-- | Minimum left bound for x. All the values of
-- type x are at least as MinL x says, as
-- required by wrap.
type family MinL (x :: Type) :: L x
-- | The kind of r in I x l r.
type family R (x :: Type) :: k
-- | Maximum right bound for x. All the values of
-- type x are at most as MaxR x says, as
-- required by wrap.
type family MaxR (x :: Type) :: R x
-- | For I x l r to be a valid interval type,
-- Interval x l r needs to be satisfied. All
-- Intervals are non-empty.
--
-- NB: When defining Interval instances, instead of
-- mentioning any necessary constraints in the instance context, mention
-- them them in IntervalCtx. By doing so, when an instance of
-- Interval x l r is satisfied, IntervalCtx x
-- l r is satisfied as well. If you don't do this, with won't
-- behave as you would expect.
class IntervalCtx x l r => Interval (x :: Type) (l :: L x) (r :: R x) where {
-- | Constraints to be satisfied for I x l r to be a valid
-- non-empty interval type.
type IntervalCtx x l r :: Constraint;
-- | Minimum value of type x contained in the interval
-- I x l r, if any. If I x l r is
-- unbounded on the left end, then it's ok to leave MinI x l
-- r undefined. If defined, it should mean the same as l.
type MinI x l r :: T x;
-- | Maximum value of type x contained in the interval
-- I x l r, if any. If I x l r is
-- unbounded on the right end, then it's ok to leave MaxI x l
-- r undefined. If defined, it should mean the same as r.
type MaxI x l r :: T x;
type IntervalCtx x l r = ();
type MinI x l r = TypeError ('Text "MinI not defined in instance ‘" ':<>: 'ShowType (Interval x l r) ':<>: 'Text "’");
type MaxI x l r = TypeError ('Text "MaxI not defined in instance ‘" ':<>: 'ShowType (Interval x l r) ':<>: 'Text "’");
}
-- | Proof that there is at least one element in the I x l
-- r interval.
--
-- No guarantees are made about the value of inhabitant other than
-- the fact that it is known to inhabit the interval. The only exception
-- to this are intervals that contain a single inhabitant, in which case
-- inhabitant will produce it. See single.
inhabitant :: Interval x l r => I x l r
-- | Wrap the x value in the interval I x l r, if
-- it fits.
--
--
-- - Consider using wrap if the interval includes all values of
-- type x.
-- - Consider using known if you have type-level knowledge about
-- the value of x.
-- - Consider using unsafe if you know that the x is
-- within the interval.
--
--
--
from :: Interval x l r => x -> Maybe (I x l r)
-- | plus' a b adds a and b.
--
-- Nothing if the result would be out of the interval. See
-- plus, too.
plus' :: Interval x l r => I x l r -> I x l r -> Maybe (I x l r)
-- | mult' a b multiplies a times b.
--
-- Nothing if the result would be out of the interval. See
-- mult, too.
mult' :: Interval x l r => I x l r -> I x l r -> Maybe (I x l r)
-- | minus' a b substracts b from a.
--
-- Nothing if the result would be out of the interval. See
-- minus, too.
minus' :: Interval x l r => I x l r -> I x l r -> Maybe (I x l r)
-- | negate' a is the additive inverse of a.
--
-- Nothing if the result would be out of the interval. See
-- negate, too.
negate' :: Interval x l r => I x l r -> Maybe (I x l r)
-- | recip' a is the multiplicative inverse of a.
--
-- Nothing if the result would be out of the interval.
recip' :: Interval x l r => I x l r -> Maybe (I x l r)
-- | div' a b divides a by b.
--
-- Nothing if the result would be out of the interval. See
-- div too.
div' :: Interval x l r => I x l r -> I x l r -> Maybe (I x l r)
-- | Obtain the x that is wrapped in the I x l r.
--
--
unwrap :: forall x l r. I x l r -> x
-- | Wrap the given x in the interval I x (MinL
-- x) (MaxR x).
--
-- This function always succeeds because the interval known to fit all
-- the values of type x.
--
--
--
-- If the interval is not as big as x:
--
--
-- - Consider using from.
-- - Consider using known if you have type-level knowledge about
-- the value of x.
-- - Consider using unsafe if you know that the x is
-- within the interval.
--
wrap :: Interval x (MinL x) (MaxR x) => x -> I x (MinL x) (MaxR x)
-- | unsafe allows you to wrap an x in an I x l
-- r, failing with error if the x is outside the
-- interval.
--
-- WARNING: This function calls from, which means that you
-- can't use it to implement from. You will have to use
-- unsafest in that case. Your code will loop indefinitely
-- otherwise.
unsafe :: forall x l r. (HasCallStack, Interval x l r) => x -> I x l r
-- | Intervals that support clamping.
class (Interval x l r) => Clamp (x :: Type) (l :: L x) (r :: R x)
-- | Wrap x in I x l r, making sure that
-- x is within the interval ends by clamping it to
-- MinI x l r if less than l, or to
-- MaxI x l r if more than r, if necessary.
clamp :: Clamp x l r => x -> I x l r
-- | Wrap x in I x l r, making sure that
-- x is within the interval ends by clamping it to
-- MinI x l r if less than l, or to
-- MaxI x l r if more than r, if necessary.
clamp :: (Clamp x l r, Known x l r (MinI x l r), Known x l r (MaxI x l r), Ord x) => x -> I x l r
-- | Intervals that can be upcasted to a larger Interval
-- type.
class (Interval x ld rd, Interval x lu ru) => Up (x :: Type) (ld :: L x) (rd :: R x) (lu :: L x) (ru :: R x)
-- | Proof that I x ld rd can be upcasted into I
-- x lu ru.
--
--
up :: Up x ld rd lu ru => I x ld rd -> I x lu ru
-- | Proof that I x ld rd can be upcasted into I
-- x lu ru.
--
--
up :: (Up x ld rd lu ru, HasCallStack) => I x ld rd -> I x lu ru
-- | Downcast I x lu ru into I x ld rd if
-- wrapped x value fits in I x ld rd.
down :: forall x lu ru ld rd. Interval x ld rd => I x lu ru -> Maybe (I x ld rd)
-- | Intervals that contain discrete elements.
class (Interval x l r) => Discrete (x :: Type) (l :: L x) (r :: R x)
-- | Predecessor. That is, the previous discrete value in the
-- interval.
--
-- Nothing if the result would be out of the interval. See
-- pred too.
pred' :: Discrete x l r => I x l r -> Maybe (I x l r)
-- | Successor. That is, the next discrete value in the
-- interval.
--
-- Nothing if the result would be out of the interval. See
-- succ too.
succ' :: Discrete x l r => I x l r -> Maybe (I x l r)
-- | Discrete Intervals where obtaining the successor
-- is knonwn to be a closed operation.
class (Discrete x l r) => Succ (x :: Type) (l :: L x) (r :: R x)
-- | succ a is the next discrete value in the interval, the
-- successor.
--
--
succ :: Succ x l r => I x l r -> I x l r
-- | Discrete Intervals where obtaining the
-- predecessor is knonwn to be a closed operation.
class (Discrete x l r) => Pred (x :: Type) (l :: L x) (r :: R x)
-- | pred a is the previous discrete value in the interval,
-- the predecessor.
--
--
pred :: Pred x l r => I x l r -> I x l r
-- | Intervals known to be inhabited by the number one.
class (Interval x l r) => One (x :: Type) (l :: L x) (r :: R x)
-- | One.
one :: One x l r => I x l r
-- | Intervals known to be inhabited by the number zero.
class (Interval x l r) => Zero (x :: Type) (l :: L x) (r :: R x)
-- | Zero.
zero :: Zero x l r => I x l r
-- | Intervals where negation is known to be a closed
-- operation.
class (Zero x l r) => Negate (x :: Type) (l :: L x) (r :: R x)
-- | Additive inverse, if it fits in the interval.
--
--
negate :: Negate x l r => I x l r -> I x l r
-- | Intervals where addition is known to be a closed
-- operation.
class (Interval x l r) => Plus (x :: Type) (l :: L x) (r :: R x)
-- | plus a b adds a and b.
--
--
plus :: Plus x l r => I x l r -> I x l r -> I x l r
-- | Intervals where multiplication is known to be a closed
-- operation.
class (Interval x l r) => Mult (x :: Type) (l :: L x) (r :: R x)
-- | mult a b multiplies a times b.
--
--
mult :: Mult x l r => I x l r -> I x l r -> I x l r
-- | Intervals where subtraction is known to be a closed
-- operation.
class (Zero x l r) => Minus (x :: Type) (l :: L x) (r :: R x)
-- | minus a b substracts b from a
--
--
minus :: Minus x l r => I x l r -> I x l r -> I x l r
-- | Intervals where division is known to be a closed
-- operation.
class (Interval x l r) => Div (x :: Type) (l :: L x) (r :: R x)
-- | div a b divides a by b.
--
--
div :: Div x l r => I x l r -> I x l r -> I x l r
-- | Proof that t is known to be within l and
-- r in I x l r.
--
-- NB: When defining Known instances, instead of mentioning
-- any necessary constraints in the instance context, mention them them
-- in KnownCtx. By doing so, when an instance of Known
-- x l r is satisfied, KnownCtx x l r is satisfied
-- as well. If you don't do this, with won't behave as you would
-- expect.
class (Interval x l r, KnownCtx x l r t) => Known (x :: Type) (l :: L x) (r :: R x) (t :: T x) where {
-- | Constraints to be satisfied by t if it is known to be within
-- the I x l r interval.
type KnownCtx x l r t :: Constraint;
type KnownCtx x l r t = ();
}
-- | Obtain a term-level representation of t as I x l
-- r.
--
-- Also consider using known, an alternative version of this
-- function designed to be used with -XTypeApplications.
known' :: Known x l r t => Proxy t -> I x l r
-- | Alternative version of known', designed to be used with
-- -XTypeApplications. It works only when x can be
-- inferred by other means.
--
--
-- > :type known
-- known :: forall {x :: Type} (t :: T x) (l :: L x) (r :: R x). Known x l r t => I x l r
--
-- > :type known @55 :: Known Word8 l r 55 => I Word8 l r
-- known @55 :: Known Word8 l r 55 => I Word8 l r
--
-- > :type known @55 @33 :: Known Word8 33 r 55 => I Word8 33 r
-- known @55 @33 :: Known Word8 33 r 55 => I Word8 33 r
--
-- > :type known @55 @33 @77 :: I Word8 33 77
-- known @55 @33 @77 :: I Word8 33 77 :: I Word8 33 77
--
-- > known @55 @33 @77 :: I Word8 33 77
-- 55
--
known :: forall {x} t l r. Known x l r t => I x l r
-- | Proof that I x l r contains a value of type x
-- whose type-level representation t :: T x satisfies a
-- Known x l r t.
class (Interval x l r) => With (x :: Type) (l :: L x) (r :: R x)
-- | Bring to scope the type-level representation of x as t ::
-- T x, together with the constraints that prove that
-- t is Known to be in the interval I x l
-- r.
--
--
with :: With x l r => I x l r -> (forall (t :: T x). Known x l r t => Proxy t -> b) -> b
-- | Minimum value in the interval, if MinI x is defined.
min :: forall x l r. Known x l r (MinI x l r) => I x l r
-- | Maximum value in the interval, if MaxI x is defined.
max :: forall x l r. Known x l r (MaxI x l r) => I x l r
-- | If an Interval contains a single inhabitant,
-- obtain it.
single :: forall x l r. (MinI x l r ~ MaxI x l r, Known x l r (MinI x l r)) => I x l r
-- | Shove an x into an interval I x l r, somehow.
--
-- Note: This class is for testing purposes only. For example, if you
-- want to generate random values of type I x l r for
-- testing purposes, all you have to do is generate random values of type
-- x and then shove them into I x l r.
--
-- Note: We don't like this too much. If there was a good way to export
-- generators for Hedgehog or QuickCheck without depending on these
-- libraries, we'd probably export that instead.
class Interval x l r => Shove (x :: Type) (l :: L x) (r :: R x)
-- | No guarantees are made about the x value that ends up in
-- I x l r. In particular, you can't expect id
-- == unwrap . shove, not even for x values
-- for which from == Just. All shove
-- guarantees is a more or less uniform distribution.
shove :: Shove x l r => x -> I x l r
-- | unsafest allows you to wrap an x in an I x
-- l r without checking whether the x is within the
-- interval ends.
--
-- WARNING: This function is fast because it doesn't do any work,
-- but also it is very dangerous because it ignores all the safety
-- supposedly given by the I x l r type. Don't use this
-- unless you have proved by other means that the x is within
-- the I x l r interval. Please use from instead,
-- or even unsafe.
unsafest :: forall x l r. x -> I x l r