Data.Sized.Builtin

This module exports Sized type and functions specialized to GHC's built-in type numeral Nat.

Main Data-types

type Sized = (Sized :: (Type -> Type) -> Nat -> Type -> Type)

type SomeSized f a = SomeSized' f Nat a

pattern SomeSized :: forall (f :: Type -> Type) a. forall (n :: Nat). SNat n -> Sized f n a -> SomeSized f a

type Ordinal = (Ordinal :: Nat -> Type)

class Dom f a => DomC f a

Instances

Dom f a => DomC f a

Defined in Data.Sized

Accessors

Length information

length :: (Dom f a, CFoldable f, KnownNat n) => Sized f n a -> Int

sLength :: (Dom f a, CFoldable f) => Sized f n a -> SNat n

null :: (Dom f a, CFoldable f) => Sized f n a -> Bool

Indexing

(!!) :: (Dom f a, CFoldable f, (1 <= m) ~ True) => Sized f m a -> Int -> a

(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c

index :: (Dom f a, CFoldable f, (1 <= m) ~ True) => Int -> Sized f m a -> a

sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c

head :: (Dom f a, CFoldable f, (0 < n) ~ True) => Sized f n a -> a

last :: (Dom f a, CFoldable f, (0 < n) ~ True) => Sized f n a -> a

uncons :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ True) => Sized f n a -> Uncons f n a

uncons' :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ True) => Sized f n a -> Uncons f n a

type Uncons f (n :: Nat) a = Uncons f n a

pattern Uncons :: forall (f :: Type -> Type) (n :: Nat) a. () => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) => a -> Sized f n1 a -> Uncons f n a

unsnoc :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ True) => Sized f n a -> Unsnoc f n a

unsnoc' :: (Dom f a, KnownNat n, CFreeMonoid f) => proxy n -> Sized f (n + 1) a -> Unsnoc f (n + 1) a

type Unsnoc f (n :: Nat) a = Unsnoc f n a

pattern Unsnoc :: forall (f :: Type -> Type) (n :: Nat) a. () => forall (n1 :: Nat). n ~ Succ n1 => Sized f n1 a -> a -> Unsnoc f n a

Slicing

tail :: (Dom f a, CFreeMonoid f) => Sized f (1 + n) a -> Sized f n a

init :: (Dom f a, CFreeMonoid f) => Sized f (n + 1) a -> Sized f n a

take :: (Dom f a, CFreeMonoid f, (n <= m) ~ True) => SNat n -> Sized f m a -> Sized f n a

takeAtMost :: (Dom f a, CFreeMonoid f) => SNat n -> Sized f m a -> Sized f (Min n m) a

drop :: (Dom f a, CFreeMonoid f, (n <= m) ~ True) => SNat n -> Sized f m a -> Sized f (m - n) a

splitAt :: (Dom f a, CFreeMonoid f, (n <= m) ~ True) => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)

splitAtMost :: (Dom f a, CFreeMonoid f) => SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)

Construction

Initialisation

empty :: (Dom f a, Monoid (f a)) => Sized f 0 a

singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f 1 a

toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a

replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a

replicate' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> Sized f n a

generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a

Concatenation

cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (n + 1) a

(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (n + 1) a

snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a

(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a

append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a

(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a

concat :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a), CFreeMonoid f, CFunctor f', CFoldable f') => Sized f' m (Sized f n a) -> Sized f (m * n) a

Zips

zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f) => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)

zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f) => Sized f n a -> Sized f n b -> Sized f n (a, b)

zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c

zipWithSame :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

unzip :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f) => Sized f n (a, b) -> (Sized f n a, Sized f n b)

unzipWith :: (Dom f a, Dom f b, Dom f c, CUnzip f) => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)

Transformation

map :: (Dom f a, Dom f b, CFreeMonoid f) => (a -> b) -> Sized f n a -> Sized f n b

reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a

intersperse :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ((2 * n) -. 1) a

nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a

sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a

sortBy :: (Dom f a, CFreeMonoid f) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a

insert :: (Dom f a, CFreeMonoid f, Ord a) => a -> Sized f n a -> Sized f (n + 1) a

insertBy :: (Dom f a, CFreeMonoid f) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (n + 1) a

Conversion

List

toList :: (Dom f a, CFoldable f) => Sized f n a -> [a]

fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a)

fromList' :: (Dom f a, CFreeMonoid f, KnownNat n) => [a] -> Maybe (Sized f n a)

unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a

unsafeFromList' :: (Dom f a, KnownNat n, CFreeMonoid f) => [a] -> Sized f n a

fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a

fromListWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> [a] -> Sized f n a

Base container

unsized :: Sized f n a -> f a

toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a)

toSized' :: (Dom f a, CFreeMonoid f, KnownNat n) => f a -> Maybe (Sized f n a)

unsafeToSized :: SNat n -> f a -> Sized f n a

unsafeToSized' :: (Dom f a, KnownNat n) => f a -> Sized f n a

toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a

toSizedWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> f a -> Sized f n a

Querying

Partitioning

type Partitioned f (n :: Nat) a = Partitioned f n a

pattern Partitioned :: forall (f :: Type -> Type) (n :: Nat) a. () => forall (n1 :: Nat) (m :: Nat). (n ~ (n1 + m), Dom f a) => SNat n1 -> Sized f n1 a -> SNat m -> Sized f m a -> Partitioned f n a

takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a

dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a

span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a

break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a

partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a

Searching

elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool

notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool

find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a

findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int

sFindIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)

findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]

sFindIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n]

elemIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int

sElemIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)

sUnsafeElemIndex :: (Dom f a, KnownNat n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)

Deprecated: Use sElemIndex instead

elemIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]

sElemIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n]

Views and Patterns

Views

Patterns

Definitions

viewCons :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a

type ConsView f (n :: Nat) a = ConsView f n a

pattern (:-) :: a -> Sized f n a -> ConsView f (Succ n) a infixr 5

pattern NilCV :: ConsView f (Zero nat) a

viewSnoc :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a

type SnocView f (n :: Nat) a = SnocView f n a

pattern (:-::) :: Sized f n a -> a -> SnocView f (n + One nat) a infixl 5

pattern NilSV :: SnocView f (Zero nat) a

pattern (:<) :: forall (f :: Type -> Type) a (n :: Nat). (Dom f a, SingI n, CFreeMonoid f) => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) => a -> Sized f n1 a -> Sized f n a infixr 5

pattern NilL :: forall f (n :: Nat) a. (KnownNat n, CFreeMonoid f, Dom f a) => n ~ 0 => Sized f n a

pattern (:>) :: forall (f :: Type -> Type) a (n :: Nat). (Dom f a, SingI n, CFreeMonoid f) => forall (n1 :: Nat). (n ~ (n1 + 1), SingI n1) => Sized f n1 a -> a -> Sized f n a infixl 5

pattern NilR :: forall f (n :: Nat) a. (CFreeMonoid f, Dom f a, SingI n) => n ~ 0 => Sized f n a