sized-wrapper-0.1.0.0: Create a Sized version of any container
CopyrightGautier DI FOLCO
LicenseBSD2
MaintainerGautier DI FOLCO <gautier.difolco@gmail.com>
StabilityUnstable
PortabilityGHC
Safe HaskellNone
LanguageHaskell2010

Data.Sized

Description

Create Sized version of any container.

Synopsis

Base type

data Sized s a Source #

Sized proofed value.

Instances

Instances details
Eq a => Eq (Sized s a) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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 Source #

Extract the Sized proven value

trustedSized :: a -> Sized s a Source #

Trusted value

unknownSized :: a -> Sized Unknown a Source #

Unknown value

data Unknown Source #

Unknown/any size

Instances

Instances details
Size Unknown Source # 
Instance details

Defined in Data.Sized

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

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

Instances

Instances details
(KnownNat n, KnownNat m, n <= m) => Size (Between n m) Source # 
Instance details

Defined in Data.Sized

Methods

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

data Exactly (n :: Nat) Source #

Exactly n

Instances

Instances details
KnownNat n => Size (Exactly n) Source # 
Instance details

Defined in Data.Sized

Methods

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

data AtLeast (n :: Nat) Source #

At least n

Instances

Instances details
KnownNat n => Size (AtLeast n) Source # 
Instance details

Defined in Data.Sized

Methods

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

data AtMost (n :: Nat) Source #

At most n

Instances

Instances details
KnownNat n => Size (AtMost n) Source # 
Instance details

Defined in Data.Sized

Methods

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

Singleton constructor

class SizedSingleton a where Source #

Singleton constructible value

Associated Types

type SizedSingletonElement a :: Type Source #

Instances

Instances details
Applicative f => SizedSingleton (f a) Source # 
Instance details

Defined in Data.Sized

Associated Types

type SizedSingletonElement (f a) Source #

Methods

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

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

Build a Sized value from a singleton value

newtype MkSizedSingletonApplicative a Source #

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

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

From container

class Size s where Source #

Convert a container from possibly any size to Sized.

Methods

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

Instances

Instances details
Size Unknown Source # 
Instance details

Defined in Data.Sized

KnownNat n => Size (AtMost n) Source # 
Instance details

Defined in Data.Sized

Methods

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

KnownNat n => Size (AtLeast n) Source # 
Instance details

Defined in Data.Sized

Methods

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

KnownNat n => Size (Exactly n) Source # 
Instance details

Defined in Data.Sized

Methods

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

(KnownNat n, KnownNat m, n <= m) => Size (Between n m) Source # 
Instance details

Defined in Data.Sized

Methods

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

class SizedFromContainer a where Source #

Used to attempt conversion from possibly any size to Sized.

Minimal complete definition

calculateSize

Methods

calculateSize :: a -> Int Source #

isAtLeast :: Int -> a -> Bool Source #

isAtMost :: Int -> a -> Bool Source #

isExactly :: Int -> a -> Bool Source #

isBetween :: Int -> Int -> a -> Bool Source #

Instances

Instances details
Foldable f => SizedFromContainer (f a) Source # 
Instance details

Defined in Data.Sized

Methods

calculateSize :: f a -> Int Source #

isAtLeast :: Int -> f a -> Bool Source #

isAtMost :: Int -> f a -> Bool Source #

isExactly :: Int -> f a -> Bool Source #

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

newtype MkSizedFromContainerFoldable a Source #

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

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

Operations

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

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

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

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 Source #

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 Source #

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 Source #

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

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

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 Source #

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 Source #

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 Source #

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 Source #

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) Source #

fmap over a Sized container

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

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

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

Give a more precise sizing

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

Give a more general sizing

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

Semigroup append

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

Concatenative operation of Sized

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

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

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

Type-level

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

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 family a <+> b where ... Source #

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 a <-> b where ... Source #

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 ... Source #

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 ... Source #

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 = ()