Data.Sized.Peano

This module exports Sized type specialized to type-level Peano numeral Nat.

Documentation

type Ordinal (n :: Nat) = Ordinal n

type Sized f (n :: Nat) = Sized f n

type ListLikeF f = (Functor f, Forall (LLF f))

Functor f such that there is instance ListLike (f a) a for any a.

Since 0.1.0.0

instLL :: forall f a. ListLikeF f :- ListLike (f a) a

instFunctor :: ListLikeF f :- Functor f

withListLikeF :: forall pxy f a b. ListLikeF f => pxy (f a) -> ((Functor f, ListLike (f a) a) => b) -> b

withListLikeF' :: ListLikeF f => f a -> ((Functor f, ListLike (f a) a) => b) -> b

data SnocView f n a where

View of the left end of sequence (snoc-side).

Since 0.1.0.0

Constructors

NilSV :: SnocView f (Zero nat) a

(:-::) :: SingI n => Sized f n a -> a -> SnocView f (Succ n) a infixl 5

data ConsView f n a where

View of the left end of sequence (cons-side).

Since 0.1.0.0

Constructors

NilCV :: ConsView f (Zero nat) a

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

data Partitioned f n a where

The type Partitioned f n a represents partitioned sequence of length n. Value Partitioned lenL ls lenR rs stands for:

• Entire sequence is divided into ls and rs, and their length are lenL and lenR resp.

• lenL + lenR = n

Since 0.1.0.0

Constructors

Partitioned :: ListLike (f a) a => Sing n -> Sized f (n :: Nat) a -> Sing m -> Sized f (m :: Nat) a -> Partitioned f (n + m) a

data SomeSized f nat a where

Sized vector with the length is existentially quantified. This type is used mostly when the return type's length cannot be statically determined beforehand.

SomeSized sn xs :: SomeSized f a stands for the Sized sequence xs of element type a and length sn.

Since 0.1.0.0

Constructors

SomeSized :: ListLike (f a) a => Sing n -> Sized f (n :: nat) a -> SomeSized f nat a

Instances

Eq (f a) => Eq (SomeSized f nat a)

Defined in Data.Sized

Methods

(==) :: SomeSized f nat a -> SomeSized f nat a -> Bool

(/=) :: SomeSized f nat a -> SomeSized f nat a -> Bool

Show (f a) => Show (SomeSized f nat a)

Defined in Data.Sized

Methods

showsPrec :: Int -> SomeSized f nat a -> ShowS

show :: SomeSized f nat a -> String

showList :: [SomeSized f nat a] -> ShowS

length :: ListLike (f a) a => Sized f n a -> Int

Returns the length of wrapped containers. If you use unsafeFromList or similar unsafe functions, this function may return different value from type-parameterized length.

Since 0.1.0.0

sLength :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> Sing n

Sing version of length.

Since 0.2.0.0

null :: ListLike (f a) a => Sized f n a -> Bool

Test if the sequence is empty or not.

Since 0.1.0.0

(!!) :: ListLike (f a) a => Sized f (Succ m) a -> Int -> a

(Unsafe) indexing with Ints. If you want to check boundary statically, use %!! or sIndex.

Since 0.1.0.0

(%!!) :: (HasOrdinal nat, ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c

Safe indexing with Ordinals.

Since 0.1.0.0

index :: ListLike (f a) a => Int -> Sized f (Succ m) a -> a

Flipped version of !!.

Since 0.1.0.0

sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c

Flipped version of %!!.

Since 0.1.0.0

head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat < n) ~ True) => Sized f n a -> b

Take the first element of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.1.0.0

last :: (HasOrdinal nat, (Zero nat < n) ~ True, ListLike (f a) b) => Sized f n a -> b

Take the last element of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.1.0.0

uncons :: ListLike (f a) b => Sized f (Succ n) a -> (b, Sized f n a)

Take the head and tail of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.1.0.0

uncons' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (b, Sized f n a)

unsnoc :: ListLike (f a) b => Sized f (Succ n) a -> (Sized f n a, b)

Take the init and last of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.1.0.0

unsnoc' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (Sized f n a, b)

tail :: (HasOrdinal nat, ListLike (f a) a) => Sized f (Succ n) a -> Sized f (n :: nat) a

Take the tail of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.1.0.0

init :: ListLike (f a) a => Sized f (Succ n) a -> Sized f n a

Take the initial segment of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.1.0.0

take :: (ListLike (f a) a, (n <= m) ~ True, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> Sized f n a

take k xs takes first k element of xs where the length of xs should be larger than k. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

takeAtMost :: (ListLike (f a) a, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> Sized f (Min n m) a

take k xs takes first k element of xs at most. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

drop :: (HasOrdinal nat, ListLike (f a) a, (n <= m) ~ True) => Sing (n :: nat) -> Sized f m a -> Sized f (m - n) a

drop k xs drops first k element of xs and returns the rest of sequence, where the length of xs should be larger than k. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

splitAt :: (ListLike (f a) a, (n <= m) ~ True, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)

splitAt k xs split xs at k, where the length of xs should be less than or equal to k. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

splitAtMost :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)

splitAtMost k xs split xs at k. If k exceeds the length of xs, then the second result value become empty. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

empty :: forall f a. (HasOrdinal nat, ListLike (f a) a) => Sized f (Zero nat :: nat) a

Empty sequence.

Since 0.1.0.0

singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a

Sequence with one element.

Since 0.1.0.0

toSomeSized :: forall nat f a. (HasOrdinal nat, ListLike (f a) a) => f a -> SomeSized f nat a

Consruct the Sized sequence from base type, but the length parameter is dynamically determined and existentially quantified; see also SomeSized.

Since 0.1.0.0

replicate :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sing n -> a -> Sized f n a

Replicates the same value.

Since 0.1.0.0

replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a

replicate with the length inferred.

Since 0.1.0.0

generate :: forall (nat :: Type) (n :: nat) (a :: Type) f. (ListLike (f a) a, HasOrdinal nat) => Sing n -> (Ordinal n -> a) -> Sized f n a

cons :: ListLike (f a) b => b -> Sized f n a -> Sized f (Succ n) a

Append an element to the head of sequence.

Since 0.1.0.0

(<|) :: ListLike (f a) b => b -> Sized f n a -> Sized f (Succ n) a infixr 5

Infix version of cons.

Since 0.1.0.0

snoc :: ListLike (f a) b => Sized f n a -> b -> Sized f (Succ n) a

Append an element to the tail of sequence.

Since 0.1.0.0

(|>) :: ListLike (f a) b => Sized f n a -> b -> Sized f (Succ n) a infixl 5

Infix version of snoc.

Since 0.1.0.0

append :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n + m) a

Append two lists.

Since 0.1.0.0

(++) :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n + m) a infixr 5

Infix version of append.

Since 0.1.0.0

concat :: forall f f' m n a. (Functor f', Foldable f', ListLike (f a) a) => Sized f' m (Sized f n a) -> Sized f (m * n) a

Concatenates multiple sequences into one.

Since 0.1.0.0

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

Zipping two sequences. Length is adjusted to shorter one.

Since 0.1.0.0

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

zip for the sequences of the same length.

Since 0.1.0.0

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

Zipping two sequences with funtion. Length is adjusted to shorter one.

Since 0.1.0.0

zipWithSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

zipWith for the sequences of the same length.

Since 0.1.0.0

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

Unzipping the sequence of tuples.

Since 0.1.0.0

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

Map function.

Since 0.1.0.0

fmap :: forall f n a b. Functor f => (a -> b) -> Sized f n a -> Sized f n b

reverse :: ListLike (f a) a => Sized f n a -> Sized f n a

Reverse function.

Since 0.1.0.0

intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. 1) a

Intersperces.

Since 0.1.0.0

nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a

Remove all duplicates.

Since 0.1.0.0

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

Sorting sequence by ascending order.

Since 0.1.0.0

sortBy :: ListLike (f a) a => (a -> a -> Ordering) -> Sized f n a -> Sized f n a

Generalized version of sort.

Since 0.1.0.0

insert :: (ListLike (f a) a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a

Insert new element into the presorted sequence.

Since 0.1.0.0

insertBy :: ListLike (f a) a => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a

Generalized version of insert.

Since 0.1.0.0

toList :: ListLike (f a) a => Sized f n a -> [a]

Convert to list.

Since 0.1.0.0

fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> [a] -> Maybe (Sized f n a)

If the given list is shorter than n, then returns Nothing Otherwise returns Sized f n a consisting of initial n element of given list.

Since 0.1.0.0

fromList' :: (ListLike (f a) a, SingI (n :: Nat)) => [a] -> Maybe (Sized f n a)

fromList with the result length inferred.

Since 0.1.0.0

unsafeFromList :: forall (nat :: Type) f (n :: nat) a. ListLike (f a) a => Sing n -> [a] -> Sized f n a

Unsafe version of fromList. If the length of the given list does not equal to n, then something unusual happens.

Since 0.1.0.0

unsafeFromList' :: (SingI (n :: Nat), ListLike (f a) a) => [a] -> Sized f n a

unsafeFromList with the result length inferred.

Since 0.1.0.0

fromListWithDefault :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sing n -> a -> [a] -> Sized f n a

Construct a Sized f n a by padding default value if the given list is short.

Since 0.1.0.0

fromListWithDefault' :: (SingI (n :: Nat), ListLike (f a) a) => a -> [a] -> Sized f n a

fromListWithDefault with the result length inferred.

Since 0.1.0.0

unsized :: Sized f n a -> f a

Forget the length and obtain the wrapped base container.

Since 0.1.0.0

toSized :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> f a -> Maybe (Sized f n a)

If the length of the input is shorter than n, then returns Nothing. Otherwise returns Sized f n a consisting of initial n element of the input.

Since 0.1.0.0

toSized' :: (ListLike (f a) a, SingI (n :: Nat)) => f a -> Maybe (Sized f n a)

toSized with the result length inferred.

Since 0.1.0.0

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

Unsafe version of toSized. If the length of the given list does not equal to n, then something unusual happens.

Since 0.1.0.0

unsafeToSized' :: (SingI (n :: Nat), ListLike (f a) a) => f a -> Sized f n a

unsafeToSized with the result length inferred.

Since 0.1.0.0

toSizedWithDefault :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> a -> f a -> Sized f n a

Construct a Sized f n a by padding default value if the given list is short.

Since 0.1.0.0

toSizedWithDefault' :: (SingI (n :: Nat), ListLike (f a) a) => a -> f a -> Sized f n a

toSizedWithDefault with the result length inferred.

Since 0.1.0.0

takeWhile :: (HasOrdinal nat, ListLike (f a) a) => (a -> Bool) -> Sized f n a -> SomeSized f nat a

Take the initial segment as long as elements satisfys the predicate.

Since 0.1.0.0

dropWhile :: (HasOrdinal nat, ListLike (f a) a) => (a -> Bool) -> Sized f n a -> SomeSized f nat a

Drop the initial segment as long as elements satisfys the predicate.

Since 0.1.0.0

span :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a

Invariant: ListLike (f a) a instance must be implemented to satisfy the following property: length (fst (span p xs)) + length (snd (span p xs)) == length xs Otherwise, this function introduces severe contradiction.

Since 0.1.0.0

break :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a

Invariant: ListLike (f a) a instance must be implemented to satisfy the following property: length (fst (break p xs)) + length (snd (break p xs)) == length xs Otherwise, this function introduces severe contradiction.

Since 0.1.0.0

partition :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a

Invariant: ListLike (f a) a instance must be implemented to satisfy the following property: length (fst (partition p xs)) + length (snd (partition p xs)) == length xs Otherwise, this function introduces severe contradiction.

Since 0.1.0.0

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

Membership test; see also notElem.

Since 0.1.0.0

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

Negation of elem.

Since 0.1.0.0

find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a

Find the element satisfying the predicate.

Since 0.1.0.0

findF :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a

Foldable version of find.

findIndex :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Maybe Int

findIndex p xs find the element satisfying p and returns its index if exists.

Since 0.1.0.0

sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)

Ordinal version of findIndex.

Since 0.1.0.0

findIndexIF :: FoldableWithIndex i f => (a -> Bool) -> Sized f n a -> Maybe i

findIndex implemented in terms of FoldableWithIndex

sFindIndexIF :: (FoldableWithIndex i f, Integral i, HasOrdinal nat, SingI n) => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n)

sFindIndex implemented in terms of FoldableWithIndex

findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int]

findIndices p xs find all elements satisfying p and returns their indices.

Since 0.1.0.0

findIndicesIF :: FoldableWithIndex i f => (a -> Bool) -> Sized f n a -> [i]

findIndices implemented in terms of FoldableWithIndex

sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => (a -> Bool) -> Sized f n a -> [Ordinal n]

Ordinal version of findIndices.

Since 0.1.0.0

sFindIndicesIF :: (FoldableWithIndex i f, Integral i, HasOrdinal nat, SingI n) => (a -> Bool) -> Sized f (n :: nat) a -> [Ordinal n]

elemIndex :: (Eq a, ListLike (f a) a) => a -> Sized f n a -> Maybe Int

Returns the index of the given element in the list, if exists.

Since 0.1.0.0

sElemIndex :: forall (n :: nat) f a. (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) => a -> Sized f n a -> Maybe (Ordinal n)

Ordinal version of elemIndex It statically checks boundary invariants. If you don't internal structure on Sized, then sUnsafeElemIndex is much faster and also safe for most cases.

Since 0.1.0.0

sUnsafeElemIndex :: forall (n :: nat) f a. (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) => a -> Sized f n a -> Maybe (Ordinal n)

elemIndices :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> [Int]

Returns all indices of the given element in the list.

Since 0.1.0.0

sElemIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a, Eq a) => a -> Sized f n a -> [Ordinal n]

Ordinal version of elemIndices

Since 0.1.0.0

viewCons :: forall f a (n :: nat). (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> ConsView f n a

Case analysis for the cons-side of sequence.

Since 0.1.0.0

viewSnoc :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> SnocView f n a

Case analysis for the snoc-side of sequence.

Since 0.1.0.0

pattern (:<) :: forall f (n :: Nat) a. ListLike (f a) a => 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. ListLike (f a) a => n ~ Z => Sized f n a

pattern (:>) :: forall f (n :: Nat) a. ListLike (f a) a => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) => Sized f n1 a -> a -> Sized f n a infixl 5

pattern NilR :: forall f (n :: Nat) a. ListLike (f a) a => n ~ Z => Sized f n a