-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Sized sequence data-types -- @package sized @version 0.1.0.0 -- | This module provides the functionality to make length-parametrized -- types from existing ListLike and Functor sequential -- types. -- -- Most of the complexity of operations for Sized f n a are the -- same as original operations for f. For example, !! is -- O(1) for Sized Vector n a but O(i) for Sized [] n a. -- -- This module also provides powerful view types and pattern synonyms to -- inspect the sized sequence. See Views and Patterns for more -- detail. module Data.Sized -- | Sized wraps a sequential type f and makes -- length-parametrized version. GHC's type natural is currently poor, so -- we adopt Peano numeral here. -- -- Here, f must be the instance of Functor and -- ListLike (f a) a for all a. This constraint -- is expressed by ListLikeF. Folding and traversing function such -- as all and foldl' is available via Foldable or -- Traversable class, if f is the instance of them. -- -- Since 0.1.0.0 data Sized f (n :: Nat) a -- | Functor f such that there is instance ListLike (f a) -- a for any a. -- -- Since 0.1.0.0 type ListLikeF f = (Functor f, Forall (LLF f)) -- | 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 data SomeSized f a SomeSized :: SNat n -> Sized f (n :: Nat) a -> SomeSized f a -- | 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 length :: ListLikeF f => Sized f n a -> Int -- | SNat version of length. -- -- Since 0.1.0.0 sLength :: SingI n => Sized f n a -> SNat n -- | Test if the sequence is empty or not. -- -- Since 0.1.0.0 null :: ListLikeF f => Sized f n a -> Bool -- | (Unsafe) indexing with Ints. If you want to check boundary -- statically, use %!! or sIndex. -- -- Since 0.1.0.0 (!!) :: ListLikeF f => Sized f (S m) a -> Int -> a -- | Safe indexing with Ordinals. -- -- Since 0.1.0.0 (%!!) :: ListLikeF f => Sized f n a -> Ordinal n -> a -- | Flipped version of !!. -- -- Since 0.1.0.0 index :: ListLikeF f => Int -> Sized f (S m) c -> c -- | Flipped version of %!!. -- -- Since 0.1.0.0 sIndex :: ListLikeF f => Ordinal n -> Sized f n c -> c -- | 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 head :: ListLikeF f => Sized f (S n) a -> a -- | 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 last :: ListLikeF f => Sized f (S n) a -> 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 :: ListLikeF f => Sized f (S n) a -> (a, Sized f n a) -- | 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 :: ListLikeF f => Sized f (S n) a -> (Sized f n a, 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 tail :: ListLikeF f => Sized f (S 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 init :: ListLikeF f => Sized f (S n) 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 take :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> Sized f m a -> Sized f n 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 takeAtMost :: ListLikeF f => SNat n -> Sized f m a -> Sized f (Min n m) 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 drop :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> Sized f m 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 splitAt :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> Sized f m a -> (Sized f n 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 splitAtMost :: ListLikeF f => SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m :-: n) a) -- | Empty sequence. -- -- Since 0.1.0.0 empty :: ListLikeF f => Sized f Z a -- | Sequence with one element. -- -- Since 0.1.0.0 singleton :: ListLikeF f => a -> Sized f One 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 toSomeSized :: ListLikeF f => f a -> SomeSized f a -- | Replicates the same value. -- -- Since 0.1.0.0 replicate :: ListLikeF f => SNat n -> a -> Sized f n a -- | replicate with the length inferred. -- -- Since 0.1.0.0 replicate' :: (SingI (n :: Nat), ListLikeF f) => a -> Sized f n a -- | Append an element to the head of sequence. -- -- Since 0.1.0.0 cons :: ListLikeF f => a -> Sized f n a -> Sized f (S n) a -- | Infix version of cons. -- -- Since 0.1.0.0 (<|) :: ListLikeF f => a -> Sized f n a -> Sized f (S n) a -- | Append an element to the tail of sequence. -- -- Since 0.1.0.0 snoc :: ListLikeF f => Sized f n a -> a -> Sized f (S n) a -- | Infix version of snoc. -- -- Since 0.1.0.0 (|>) :: ListLikeF f => Sized f n a -> a -> Sized f (S n) a -- | Append two lists. -- -- Since 0.1.0.0 append :: ListLikeF f => Sized f n a -> Sized f m a -> Sized f (n :+ m) a -- | Infix version of append. -- -- Since 0.1.0.0 (++) :: ListLikeF f => Sized f n a -> Sized f m a -> Sized f (n :+ m) a -- | Concatenates multiple sequences into one. -- -- Since 0.1.0.0 concat :: (ListLikeF f, ListLikeF f') => Sized f' m (Sized f n a) -> Sized f (m :* n) a -- | Zipping two sequences. Length is adjusted to shorter one. -- -- Since 0.1.0.0 zip :: ListLikeF f => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) -- | zip for the sequences of the same length. -- -- Since 0.1.0.0 zipSame :: ListLikeF f => Sized f n a -> Sized f n b -> Sized f n (a, b) -- | Zipping two sequences with funtion. Length is adjusted to shorter one. -- -- Since 0.1.0.0 zipWith :: ListLikeF f => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c -- | zipWith for the sequences of the same length. -- -- Since 0.1.0.0 zipWithSame :: ListLikeF f => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c -- | Unzipping the sequence of tuples. -- -- Since 0.1.0.0 unzip :: ListLikeF f => Sized f n (a, b) -> (Sized f n a, Sized f n b) -- | Map function. -- -- Since 0.1.0.0 map :: Functor f => (a -> b) -> Sized f n a -> Sized f n b -- | Reverse function. -- -- Since 0.1.0.0 reverse :: ListLikeF f => Sized f n a -> Sized f n a -- | Intersperces. -- -- Since 0.1.0.0 intersperse :: ListLikeF f => a -> Sized f n a -> Sized f ((Two :* n) :-: One) a -- | Remove all duplicates. -- -- Since 0.1.0.0 nub :: (ListLikeF f, Eq a) => Sized f n a -> SomeSized f a -- | Sorting sequence by ascending order. -- -- Since 0.1.0.0 sort :: (ListLikeF f, Ord a) => Sized f n a -> Sized f n a -- | Generalized version of sort. -- -- Since 0.1.0.0 sortBy :: ListLikeF f => (a -> a -> Ordering) -> Sized f n a -> Sized f n a -- | Insert new element into the presorted sequence. -- -- Since 0.1.0.0 insert :: (ListLikeF f, Ord a) => a -> Sized f n a -> Sized f (S n) a -- | Generalized version of insert. -- -- Since 0.1.0.0 insertBy :: ListLikeF f => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (S n) a -- | Convert to list. -- -- Since 0.1.0.0 toList :: ListLikeF f => Sized f n a -> [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 :: ListLikeF f => SNat n -> [a] -> Maybe (Sized f n a) -- | fromList with the result length inferred. -- -- Since 0.1.0.0 fromList' :: (ListLikeF f, SingI (n :: Nat)) => [a] -> Maybe (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 :: ListLikeF f => SNat n -> [a] -> Sized f n a -- | unsafeFromList with the result length inferred. -- -- Since 0.1.0.0 unsafeFromList' :: (SingI (n :: Nat), ListLikeF 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 fromListWithDefault :: ListLikeF f => SNat n -> a -> [a] -> Sized f n a -- | fromListWithDefault with the result length inferred. -- -- Since 0.1.0.0 fromListWithDefault' :: (SingI (n :: Nat), ListLikeF f) => a -> [a] -> Sized f n a -- | Forget the length and obtain the wrapped base container. -- -- Since 0.1.0.0 unsized :: Sized f n a -> f 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 :: ListLikeF f => SNat n -> f a -> Maybe (Sized f n a) -- | toSized with the result length inferred. -- -- Since 0.1.0.0 toSized' :: (ListLikeF f, SingI (n :: Nat)) => f a -> Maybe (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 :: SNat n -> f a -> Sized f n a -- | unsafeToSized with the result length inferred. -- -- Since 0.1.0.0 unsafeToSized' :: (SingI (n :: Nat), ListLikeF f) => 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 :: ListLikeF f => SNat n -> a -> f a -> Sized f n a -- | toSizedWithDefault with the result length inferred. -- -- Since 0.1.0.0 toSizedWithDefault' :: (SingI (n :: Nat), ListLikeF f) => a -> f a -> Sized f n a -- | The type Partitioned f n a represents partitioned sequence of -- length n. Value Partitioned lenL ls lenR rs stands -- for: -- -- -- -- Since 0.1.0.0 data Partitioned f n a Partitioned :: SNat n -> Sized f (n :: Nat) a -> SNat m -> Sized f (m :: Nat) a -> Partitioned f (n :+ m) a -- | Take the initial segment as long as elements satisfys the predicate. -- -- Since 0.1.0.0 takeWhile :: ListLikeF f => (a -> Bool) -> Sized f n a -> SomeSized f a -- | Drop the initial segment as long as elements satisfys the predicate. -- -- Since 0.1.0.0 dropWhile :: ListLikeF f => (a -> Bool) -> Sized f n a -> SomeSized f 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 span :: ListLikeF f => (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 break :: ListLikeF f => (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 partition :: ListLikeF f => (a -> Bool) -> Sized f n a -> Partitioned f n a -- | Membership test; see also notElem. -- -- Since 0.1.0.0 elem :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool -- | Negation of elem. -- -- Since 0.1.0.0 notElem :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool -- | Find the element satisfying the predicate. -- -- Since 0.1.0.0 find :: ListLikeF f => (a -> Bool) -> Sized f n a -> Maybe a -- | findIndex p xs find the element satisfying p -- and returns its index if exists. -- -- Since 0.1.0.0 findIndex :: ListLikeF f => (a -> Bool) -> Sized f n a -> Maybe Int -- | Ordinal version of findIndex. -- -- Since 0.1.0.0 sFindIndex :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) -- | findIndices p xs find all elements satisfying -- p and returns their indices. -- -- Since 0.1.0.0 findIndices :: ListLikeF f => (a -> Bool) -> Sized f n a -> [Int] -- | Ordinal version of findIndices. -- -- Since 0.1.0.0 sFindIndices :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> [Ordinal n] -- | Returns the index of the given element in the list, if exists. -- -- Since 0.1.0.0 elemIndex :: (Eq a, ListLikeF f) => a -> Sized f n a -> Maybe Int -- | Ordinal version of elemIndex -- -- Since 0.1.0.0 sElemIndex :: (SingI n, ListLikeF f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n) -- | Returns all indices of the given element in the list. -- -- Since 0.1.0.0 elemIndices :: (ListLikeF f, Eq a) => a -> Sized f n a -> [Int] -- | Ordinal version of elemIndices -- -- Since 0.1.0.0 sElemIndices :: (SingI n, ListLikeF f, Eq a) => a -> Sized f n a -> [Ordinal n] -- | Case analysis for the cons-side of sequence. -- -- Since 0.1.0.0 viewCons :: (SingI n, ListLikeF f) => Sized f n a -> ConsView f n a -- | View of the left end of sequence (cons-side). -- -- Since 0.1.0.0 data ConsView f n a NilCV :: ConsView f Z a (::-) :: a -> Sized f n a -> ConsView f (S n) a -- | Case analysis for the snoc-side of sequence. -- -- Since 0.1.0.0 viewSnoc :: (SingI n, ListLikeF f) => Sized f n a -> SnocView f n a -- | View of the left end of sequence (snoc-side). -- -- Since 0.1.0.0 data SnocView f n a NilSV :: SnocView f Z a (:-::) :: Sized f n a -> a -> SnocView f (S n) a instance Show (f a) => Show (SomeSized f a) instance Typeable SomeSized instance Eq (f a) => Eq (SomeSized f a)