Data.Sized

Create Sized version of any container.

Base type

data Sized s a

Sized proofed value.

Instances

Eq a => Eq (Sized s a)

Defined in Data.Sized

Methods

(==) :: Sized s a -> Sized s a -> Bool

(/=) :: Sized s a -> Sized s a -> Bool

Ord a => Ord (Sized s a)

Defined in Data.Sized

Methods

compare :: Sized s a -> Sized s a -> Ordering

(<) :: Sized s a -> Sized s a -> Bool

(<=) :: Sized s a -> Sized s a -> Bool

(>) :: Sized s a -> Sized s a -> Bool

(>=) :: Sized s a -> Sized s a -> Bool

max :: Sized s a -> Sized s a -> Sized s a

min :: Sized s a -> Sized s a -> Sized s a

Show a => Show (Sized s a)

Defined in Data.Sized

Methods

showsPrec :: Int -> Sized s a -> ShowS

show :: Sized s a -> String

showList :: [Sized s a] -> ShowS

$sel:getSized:Sized :: Sized s a -> a

Extract the Sized proven value

trustedSized :: a -> Sized s a

Trusted value

unknownSized :: a -> Sized Unknown a

Unknown value

data Unknown

Unknown/any size

Instances

Size Unknown

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized Unknown a)

data Between (n :: Nat) (m :: Nat)

Between (included) '(n..m)'

Instances

(KnownNat n, KnownNat m, n <= m) => Size (Between n m)

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized (Between n m) a)

data Exactly (n :: Nat)

Exactly n

Instances

KnownNat n => Size (Exactly n)

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized (Exactly n) a)

data AtLeast (n :: Nat)

At least n

Instances

KnownNat n => Size (AtLeast n)

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized (AtLeast n) a)

data AtMost (n :: Nat)

At most n

Instances

KnownNat n => Size (AtMost n)

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized (AtMost n) a)

Singleton constructor

class SizedSingleton a where

Singleton constructible value

Associated Types

type SizedSingletonElement a :: Type

Methods

sizedSingleton :: Proxy a -> SizedSingletonElement a -> a

Instances

Applicative f => SizedSingleton (f a)

Defined in Data.Sized

Associated Types

type SizedSingletonElement (f a)

Methods

sizedSingleton :: Proxy (f a) -> SizedSingletonElement (f a) -> f a

singleton :: SizedSingleton a => Proxy a -> SizedSingletonElement a -> Sized (Exactly 1) a

Build a Sized value from a singleton value

newtype MkSizedSingletonApplicative a

Build SizedSingleton for Applicative defined types to be used with DerivingVia:

deriving instance SizedSingleton [a] via (MkSizedSingletonApplicative [a])

Constructors

MkSizedSingletonApplicative a

From container

class Size s where

Convert a container from possibly any size to Sized.

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized s a)

Instances

Size Unknown

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized Unknown a)

KnownNat n => Size (AtMost n)

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized (AtMost n) a)

KnownNat n => Size (AtLeast n)

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized (AtLeast n) a)

KnownNat n => Size (Exactly n)

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized (Exactly n) a)

(KnownNat n, KnownNat m, n <= m) => Size (Between n m)

Defined in Data.Sized

Methods

sized :: SizedFromContainer a => a -> Maybe (Sized (Between n m) a)

class SizedFromContainer a where

Used to attempt conversion from possibly any size to Sized.

Minimal complete definition

calculateSize

Methods

calculateSize :: a -> Int

isAtLeast :: Int -> a -> Bool

isAtMost :: Int -> a -> Bool

isExactly :: Int -> a -> Bool

isBetween :: Int -> Int -> a -> Bool

Instances

Foldable f => SizedFromContainer (f a)

Defined in Data.Sized

Methods

calculateSize :: f a -> Int

isAtLeast :: Int -> f a -> Bool

isAtMost :: Int -> f a -> Bool

isExactly :: Int -> f a -> Bool

isBetween :: Int -> Int -> f a -> Bool

newtype MkSizedFromContainerFoldable a

Build MkSizedFromContainerFoldable for Foldable defined types to be used with DerivingVia:

deriving instance SizedFromContainer [a] via (MkSizedFromContainerFoldable [a])

Constructors

MkSizedFromContainerFoldable a

Operations

overSized :: (a -> b) -> Sized s a -> Sized s b

Wrap and unwrap Sized (unsafe, be sure f is size-conservative)

overSized2 :: (a -> b -> c) -> Sized s a -> Sized s b -> Sized s c

Wrap and unwrap Sized (unsafe, be sure f is size-conservative)

overSized3 :: (a -> b -> c -> d) -> Sized s a -> Sized s b -> Sized s c -> Sized s d

Wrap and unwrap Sized (unsafe, be sure f is size-conservative)

overSized4 :: (a -> b -> c -> d -> e) -> Sized s a -> Sized s b -> Sized s c -> Sized s d -> Sized s e

Wrap and unwrap Sized (unsafe, be sure f is size-conservative)

overSized5 :: (a -> b -> c -> d -> e -> f) -> Sized s a -> Sized s b -> Sized s c -> Sized s d -> Sized s e -> Sized s f

Wrap and unwrap Sized (unsafe, be sure f is size-conservative)

trustedChangeOverSized :: (a -> b) -> Sized s0 a -> Sized s1 b

Wrap and unwrap Sized (unsafe, be sure f is respects output size)

trustedChangeOverSized2 :: (a -> b -> c) -> Sized s0 a -> Sized s1 b -> Sized s2 c

Wrap and unwrap Sized (unsafe, be sure f is respects output size)

trustedChangeOverSized3 :: (a -> b -> c -> d) -> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d

Wrap and unwrap Sized (unsafe, be sure f is respects output size)

trustedChangeOverSized4 :: (a -> b -> c -> d -> e) -> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d -> Sized s4 e

Wrap and unwrap Sized (unsafe, be sure f is respects output size)

trustedChangeOverSized5 :: (a -> b -> c -> d -> e -> f) -> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d -> Sized s4 e -> Sized s5 f

Wrap and unwrap Sized (unsafe, be sure f is respects output size)

fmapSized :: Functor f => (a -> b) -> Sized s (f a) -> Sized s (f b)

fmap over a Sized container

withSized :: (a -> Maybe b) -> Sized s a -> b

Apply an unsafe function over empty, which is safe over Sized

precise :: (SizedFromContainer a, Size s) => Sized s' a -> Maybe (Sized s a)

Give a more precise sizing

approximate :: IsMoreGeneral s s' => Sized s' a -> Sized s a

Give a more general sizing

(<<>>) :: Semigroup a => Sized s a -> Sized s' a -> Sized (s <+> s') a infixr 6

Semigroup append

withSizedAppend :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <+> s') c

Concatenative operation of Sized

withSizedRetract :: (a -> b) -> Sized s a -> Sized (RestrictAtMost s) b

withSizedSubtract :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <-> s') c

withSizedProduct :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <*> s') c

Type-level

type family IsMoreGeneral general restrictive :: Constraint where ...

Equations

IsMoreGeneral (AtLeast n) (AtLeast m) = n <= m

IsMoreGeneral (AtMost n) (AtMost m) = m <= n

IsMoreGeneral (AtLeast n) (Exactly m) = n <= m

IsMoreGeneral (AtMost n) (Exactly m) = m <= n

IsMoreGeneral (AtLeast n) (Between m o) = n <= m

IsMoreGeneral (AtMost n) (Between m o) = o <= n

IsMoreGeneral (Between n m) (Between o p) = (n <= o, p <= m)

IsMoreGeneral (Between n m) (Exactly o) = (n <= o, o <= m)

IsMoreGeneral Unknown a = ()

type IsNotEmpty s = IsMoreGeneral s (Exactly 1)

type family a <+> b where ...

Equations

Unknown <+> b = Unknown

a <+> Unknown = Unknown

(AtMost n) <+> (AtMost m) = AtMost (n + m)

(AtMost n) <+> (Exactly m) = AtMost (n + m)

(Exactly n) <+> (Exactly m) = Exactly (n + m)

(Exactly n) <+> (AtMost m) = AtMost (n + m)

(Exactly n) <+> (AtLeast m) = AtLeast (n + m)

(AtLeast n) <+> (Exactly m) = AtLeast (n + m)

(AtLeast n) <+> (AtLeast m) = AtLeast (n + m)

(AtLeast n) <+> (AtMost m) = Between n (n + m)

(AtMost n) <+> (AtLeast m) = Between m (n + m)

(AtLeast n) <+> (Between m o) = Between (n + m) (n + o)

(AtMost n) <+> (Between m o) = Between m (n + o)

(Between n m) <+> (Exactly o) = Between (n + o) (m + o)

(Exactly o) <+> (Between n m) = Between (n + o) (m + o)

(Between m o) <+> (AtLeast n) = Between (n + m) (n + o)

(Between m o) <+> (AtMost n) = Between m (n + o)

(Between n m) <+> (Between o p) = Between (n + o) (m + p)

type family RestrictAtMost a where ...

Equations

RestrictAtMost Unknown = Unknown

RestrictAtMost (AtMost n) = AtMost n

RestrictAtMost (AtLeast n) = AtLeast 0

RestrictAtMost (Between n m) = AtMost m

RestrictAtMost (Exactly n) = AtMost n

type family a <-> b where ...

Equations

Unknown <-> b = Unknown

a <-> Unknown = Unknown

(AtMost n) <-> (AtMost m) = AtMost (n - m)

(Exactly n) <-> (AtMost m) = AtMost (n - m)

(AtMost n) <-> (Exactly m) = AtMost (n - m)

(Exactly n) <-> (Exactly m) = Exactly (n - m)

(Exactly n) <-> (AtLeast m) = AtLeast (n - m)

(AtLeast n) <-> (Exactly m) = AtLeast (n - m)

(AtLeast n) <-> (AtLeast m) = AtLeast (n - m)

(AtLeast n) <-> (AtMost m) = AtLeast (n - m)

(AtMost n) <-> (AtLeast m) = AtLeast 0

(AtLeast n) <-> (Between m o) = AtLeast (m - n)

(AtMost n) <-> (Between m o) = Between (m - n) o

(Between n m) <-> (Exactly o) = Between (n - o) (m - o)

(Exactly o) <-> (Between n m) = Between (o - n) (o - m)

(Between m o) <-> (AtLeast n) = AtLeast 0

(Between m o) <-> (AtMost n) = Between m (o - n)

(Between n m) <-> (Between o p) = Between (n - o) (m - p)

type family a <*> b where ...

Equations

Unknown <*> b = Unknown

a <*> Unknown = Unknown

(AtMost n) <*> (AtMost m) = AtMost (n * m)

(Exactly n) <*> (AtMost m) = AtMost (n * m)

(AtMost n) <*> (Exactly m) = AtMost (n * m)

(Exactly n) <*> (Exactly m) = Exactly (n * m)

(AtLeast n) <*> (Exactly m) = AtLeast (n * m)

(Exactly n) <*> (AtLeast m) = AtLeast (n * m)

(AtLeast n) <*> (AtLeast m) = AtLeast (n * m)

(AtLeast n) <*> (AtMost m) = AtLeast 0

(AtMost n) <*> (AtLeast m) = AtLeast 0

(AtLeast n) <*> (Between m o) = AtLeast (m * n)

(AtMost n) <*> (Between m o) = AtLeast 0

(Between n m) <*> (Exactly o) = Between (n * o) (m * o)

(Exactly o) <*> (Between n m) = Between (n * o) (m * o)

(Between m o) <*> (AtLeast n) = AtLeast (m * n)

(Between m o) <*> (AtMost n) = AtLeast 0

(Between n m) <*> (Between o p) = Between (n * o) (m * p)

type family Includes (sized :: Type) (size :: Nat) :: Constraint where ...

Equations

Includes (AtLeast n) m = n <= m

Includes (AtMost n) m = m <= n

Includes (Between n m) o = (n <= o, o <= m)

Includes Unknown a = ()