Foundation.List.SList

A Nat-sized list abstraction

Using this module is limited to GHC 7.10 and above.

Documentation

data SList n a

toSList :: forall n a. (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (SList n a)

unSList :: SList n a -> [a]

length :: forall a n. (KnownNat n, NatWithinBound Int n) => SList n a -> Int

create :: forall a n. KnownNat n => (Integer -> a) -> SList n a

createFrom :: forall a n start. (KnownNat n, KnownNat start) => Proxy start -> (Integer -> a) -> SList n a

empty :: SList 0 a

singleton :: a -> SList 1 a

uncons :: CmpNat n 0 ~ GT => SList n a -> (a, SList (n - 1) a)

cons :: a -> SList n a -> SList (n + 1) a

map :: (a -> b) -> SList n a -> SList n b

elem :: Eq a => a -> SList n a -> Bool

foldl :: (b -> a -> b) -> b -> SList n a -> b

append :: SList n a -> SList m a -> SList (n + m) a

minimum :: (Ord a, CmpNat n 0 ~ GT) => SList n a -> a

maximum :: (Ord a, CmpNat n 0 ~ GT) => SList n a -> a

head :: CmpNat n 0 ~ GT => SList n a -> a

tail :: CmpNat n 0 ~ GT => SList n a -> SList (n - 1) a

take :: forall a m n. (KnownNat m, NatWithinBound Int m, m <= n) => SList n a -> SList m a

drop :: forall a d m n. (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => SList n a -> SList m a

zip :: SList n a -> SList n b -> SList n (a, b)

zip3 :: SList n a -> SList n b -> SList n c -> SList n (a, b, c)

zip4 :: SList n a -> SList n b -> SList n c -> SList n d -> SList n (a, b, c, d)

zip5 :: SList n a -> SList n b -> SList n c -> SList n d -> SList n e -> SList n (a, b, c, d, e)

zipWith :: (a -> b -> x) -> SList n a -> SList n b -> SList n x

zipWith3 :: (a -> b -> c -> x) -> SList n a -> SList n b -> SList n c -> SList n x

zipWith4 :: (a -> b -> c -> d -> x) -> SList n a -> SList n b -> SList n c -> SList n d -> SList n x

zipWith5 :: (a -> b -> c -> d -> e -> x) -> SList n a -> SList n b -> SList n c -> SList n d -> SList n e -> SList n x

replicateM :: forall n m a. (n <= 1048576, Monad m, KnownNat n) => m a -> m (SList n a)