Copyright | Gautier DI FOLCO |
---|---|

License | BSD2 |

Maintainer | Gautier DI FOLCO <gautier.difolco@gmail.com> |

Stability | Unstable |

Portability | GHC |

Safe Haskell | None |

Language | Haskell2010 |

Create Sized version of any container.

## Synopsis

- data Sized s a
- $sel:getSized:Sized :: Sized s a -> a
- trustedSized :: a -> Sized s a
- unknownSized :: a -> Sized Unknown a
- data Unknown
- data Between (n :: Nat) (m :: Nat)
- data Exactly (n :: Nat)
- data AtLeast (n :: Nat)
- data AtMost (n :: Nat)
- class SizedSingleton a where
- type SizedSingletonElement a :: Type
- sizedSingleton :: Proxy a -> SizedSingletonElement a -> a

- singleton :: SizedSingleton a => Proxy a -> SizedSingletonElement a -> Sized (Exactly 1) a
- newtype MkSizedSingletonApplicative a = MkSizedSingletonApplicative a
- class Size s where
- sized :: SizedFromContainer a => a -> Maybe (Sized s a)

- class SizedFromContainer a where
- newtype MkSizedFromContainerFoldable a = MkSizedFromContainerFoldable a
- overSized :: (a -> b) -> Sized s a -> Sized s b
- overSized2 :: (a -> b -> c) -> Sized s a -> Sized s b -> Sized s c
- overSized3 :: (a -> b -> c -> d) -> Sized s a -> Sized s b -> Sized s c -> Sized s d
- overSized4 :: (a -> b -> c -> d -> e) -> Sized s a -> Sized s b -> Sized s c -> Sized s d -> Sized s e
- 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
- trustedChangeOverSized :: (a -> b) -> Sized s0 a -> Sized s1 b
- trustedChangeOverSized2 :: (a -> b -> c) -> Sized s0 a -> Sized s1 b -> Sized s2 c
- trustedChangeOverSized3 :: (a -> b -> c -> d) -> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d
- trustedChangeOverSized4 :: (a -> b -> c -> d -> e) -> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d -> Sized s4 e
- 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
- fmapSized :: Functor f => (a -> b) -> Sized s (f a) -> Sized s (f b)
- withSized :: (a -> Maybe b) -> Sized s a -> b
- precise :: (SizedFromContainer a, Size s) => Sized s' a -> Maybe (Sized s a)
- approximate :: IsMoreGeneral s s' => Sized s' a -> Sized s a
- (<<>>) :: Semigroup a => Sized s a -> Sized s' a -> Sized (s <+> s') a
- withSizedAppend :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <+> s') c
- 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 family IsMoreGeneral general restrictive :: Constraint where ...
- type IsNotEmpty s = IsMoreGeneral s (Exactly 1)
- type family a <+> b where ...
- type family RestrictAtMost a where ...
- type family a <-> b where ...
- type family a <*> b where ...
- type family Includes (sized :: Type) (size :: Nat) :: Constraint where ...

# Base type

Sized proofed value.

$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

Unknown/any size

# Singleton constructor

class SizedSingleton a where Source #

Singleton constructible value

type SizedSingletonElement a :: Type Source #

sizedSingleton :: Proxy a -> SizedSingletonElement a -> a Source #

#### Instances

Applicative f => SizedSingleton (f a) Source # | |

Defined in Data.Sized type SizedSingletonElement (f a) Source # 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

Convert a container from possibly any size to `Sized`

.

#### Instances

Size Unknown Source # | |

Defined in Data.Sized | |

KnownNat n => Size (AtMost n) Source # | |

Defined in Data.Sized | |

KnownNat n => Size (AtLeast n) Source # | |

Defined in Data.Sized | |

KnownNat n => Size (Exactly n) Source # | |

Defined in Data.Sized | |

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

Defined in Data.Sized |

class SizedFromContainer a where Source #

Used to attempt conversion from possibly any size to `Sized`

.

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)

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 #

# Type-level

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

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

type family a <+> b where ... Source #

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

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

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 #

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