sized 0.1.0.0 → 0.2.0.0
raw patch · 6 files changed
+912/−409 lines, 6 filesdep +deepseqdep +equational-reasoningdep +hashabledep ~basedep ~type-natural
Dependencies added: deepseq, equational-reasoning, hashable, lens, mono-traversable, singletons
Dependency ranges changed: base, type-natural
Files
- Data/Sized.hs +550/−347
- Data/Sized/Builtin.hs +45/−0
- Data/Sized/Flipped.hs +93/−0
- Data/Sized/Internal.hs +161/−54
- Data/Sized/Peano.hs +45/−0
- sized.cabal +18/−8
Data/Sized.hs view
@@ -1,14 +1,17 @@-{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFoldable #-}-{-# LANGUAGE DeriveFunctor, DeriveTraversable, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving #-}-{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms #-}-{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction #-}-{-# LANGUAGE PatternSynonyms, PolyKinds, ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators, ViewPatterns #-}+{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, DataKinds #-}+{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable, ExplicitNamespaces, FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms #-}+{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction #-}+{-# LANGUAGE PatternSynonyms, PolyKinds, ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving, TypeApplications, TypeFamilies #-}+{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-} {-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}+{-# OPTIONS_GHC -fenable-rewrite-rules #-} -- | 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@.@@ -17,12 +20,15 @@ -- inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail. module Data.Sized ( -- * Main Data-types- Sized(), ListLikeF, SomeSized(..),+ Sized(), SomeSized(..),+ instLL, instFunctor, ListLikeF,+ withListLikeF, withListLikeF', -- * Accessors -- ** Length information length, sLength, null, -- ** Indexing- (!!), (%!!), index, sIndex, head, last, uncons, unsnoc,+ (!!), (%!!), index, sIndex, head, last,+ uncons, uncons', unsnoc, unsnoc', -- ** Slicing tail, init, take, takeAtMost, drop, splitAt, splitAtMost, -- * Construction@@ -33,7 +39,7 @@ -- ** Zips zip, zipSame, zipWith, zipWithSame, unzip, -- * Transformation- map, reverse, intersperse, nub, sort, sortBy, insert, insertBy,+ map, fmap, reverse, intersperse, nub, sort, sortBy, insert, insertBy, -- * Conversion -- ** List toList, fromList, fromList', unsafeFromList, unsafeFromList',@@ -47,8 +53,10 @@ Partitioned(..), takeWhile, dropWhile, span, break, partition, -- ** Searching- elem, notElem, find, findIndex, sFindIndex, findIndices, sFindIndices,- elemIndex, sElemIndex, elemIndices, sElemIndices,+ elem, notElem, find, findF, findIndex, findIndexIF,+ sFindIndex, sFindIndexIF,+ findIndices, findIndicesIF, sFindIndices, sFindIndicesIF,+ elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices, -- * Views and Patterns -- $ViewsAndPatterns @@ -66,18 +74,37 @@ import Data.Sized.Internal -import qualified Data.ListLike as LL-import Data.Proxy (Proxy (..))-import Data.Type.Monomorphic-import Data.Type.Natural-import Data.Type.Ordinal (Ordinal, ordToInt)-import Data.Typeable (Typeable)-import Prelude (Bool (..), Enum (..), Eq (..),- Functor (..), Int, Maybe (..), Num (..),- Ord (..), Ordering, Show (..), flip,- undefined, ($), (.))-import qualified Prelude as P-import Unsafe.Coerce (unsafeCoerce)+import Control.Applicative ((<$>), (<*>))+import Control.Lens.Indexed (FoldableWithIndex (..), ifind)+import Data.Foldable (Foldable)+import qualified Data.Foldable as F+import Data.Kind (Type)+import qualified Data.List as L+import Data.ListLike (ListLike)+import qualified Data.ListLike as LL+import Data.Monoid (Endo (..), First (..))+import qualified Data.Sequence as Seq+import Data.Singletons.Prelude (PNum (..), POrd (..), SOrd (..))+import Data.Singletons.Prelude (Sing (..), SingI (..))+import Data.Singletons.Prelude (withSing, withSingI)+import Data.Singletons.Prelude.Enum (PEnum (..))+import Data.Type.Monomorphic (Monomorphic (..))+import Data.Type.Monomorphic (Monomorphicable (..))+import qualified Data.Type.Natural as Peano+import Data.Type.Natural.Class+import Data.Type.Ordinal (HasOrdinal, Ordinal (..))+import Data.Type.Ordinal (ordToInt, unsafeFromInt)+import Data.Typeable (Typeable)+import qualified Data.Vector as V+import qualified Data.Vector.Storable as SV+import qualified Data.Vector.Unboxed as UV+import qualified GHC.TypeLits as TL+import Prelude (Bool (..), Enum (..), Eq (..))+import Prelude (Functor, Int, Maybe (..))+import Prelude (Num (..), Ord (..), Ordering)+import Prelude (Show (..), flip, fst, ($), (.))+import qualified Prelude as P+import Unsafe.Coerce (unsafeCoerce) -------------------------------------------------------------------------------- -- Main data-types@@ -91,18 +118,25 @@ -- @xs@ of element type @a@ and length @sn@. -- -- Since 0.1.0.0-data SomeSized f a where- SomeSized :: (ListLikeF f, SingI n)- => SNat n- -> Sized f (n :: Nat) a- -> SomeSized f a+data SomeSized f nat a where+ SomeSized :: (ListLike (f a) a)+ => Sing n+ -> Sized f (n :: nat) a+ -> SomeSized f nat a deriving instance Typeable SomeSized -deriving instance Show (f a) => Show (SomeSized f a)-instance Eq (f a) => Eq (SomeSized f a) where+instance Show (f a) => Show (SomeSized f nat a) where+ showsPrec d (SomeSized _ s) = P.showParen (d > 9) $+ P.showString "SomeSized _ " . showsPrec 10 s+instance Eq (f a) => Eq (SomeSized f nat a) where (SomeSized _ (Sized xs)) == (SomeSized _ (Sized ys)) = xs == ys +demote' :: HasOrdinal nat => Sing (n :: nat) -> MonomorphicRep (Sing :: nat -> Type)+demote' = demote . Monomorphic+{-# SPECIALISE demote' :: Sing (n :: TL.Nat) -> P.Integer #-}+{-# SPECIALISE demote' :: Sing (n :: Peano.Nat) -> P.Integer #-}+ -------------------------------------------------------------------------------- -- Accessors --------------------------------------------------------------------------------@@ -114,101 +148,152 @@ -- | 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-length = givenListLikeF LL.length . runSized-{-# INLINE length #-}+length :: ListLike (f a) a => Sized f n a -> Int+length = LL.length . runSized+{-# INLINE [1] length #-}+{-# RULES+"length/0" [~1] forall (xs :: Sized f 0 a).+ length xs = 0+"length/Z" [~1] forall (xs :: Sized f 'Peano.Z a).+ length xs = 0+ #-} --- | @SNat@ version of 'length'.--- --- Since 0.1.0.0-sLength :: SingI n => Sized f n a -> SNat n-sLength _ = sing-{-# INLINE sLength #-}+-- | @Sing@ version of 'length'.+--+-- Since 0.2.0.0+sLength :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a)+ => Sized f n a -> Sing n+sLength (Sized xs) =+ case promote (P.fromIntegral $ LL.length xs) of+ Monomorphic (n :: Sing (k :: nat)) -> unsafeCoerce n+{-# INLINE[2] sLength #-}+{-# RULES+"sLength/KnownNat" [~1] forall (xs :: TL.KnownNat n => Sized f n a).+ sLength xs = sing :: Sing n+"sLength/SingI" [~2] forall (xs :: SingI n => Sized f n a).+ sLength xs = sing :: Sing n+ #-} -- | Test if the sequence is empty or not.--- +-- -- Since 0.1.0.0-null :: ListLikeF f => Sized f n a -> Bool-null = givenListLikeF' LL.null-{-# INLINE [2] null #-}+null :: ListLike (f a) a => Sized f n a -> Bool+null = LL.null . runSized+{-# INLINE CONLIKE [1] null #-} {-# RULES-"null/Zero" forall (xs :: Sized f Z a).+"null/0" [~1] forall (xs :: Sized f 0 a). null xs = True-"null/Succ" forall (xs :: Sized f (S n) a).- null xs = False- #-} +"null/Z" [~1] forall (xs :: Sized f 'Peano.Z a).+ null xs = True+#-}+ -------------------------------------------------------------------------------- --- Indexing -------------------------------------------------------------------------------- -- | (Unsafe) indexing with @Int@s. -- If you want to check boundary statically, use '%!!' or 'sIndex'.--- +-- -- Since 0.1.0.0-(!!) :: (ListLikeF f) => Sized f (S m) a -> Int -> a-Sized xs !! n = withListLikeF' xs $ LL.index xs n+(!!) :: (ListLike (f a) a) => Sized f (Succ m) a -> Int -> a+Sized xs !! n = LL.index xs n {-# INLINE (!!) #-} -- | Safe indexing with 'Ordinal's.--- +-- -- Since 0.1.0.0-(%!!) :: ListLikeF f => Sized f n a -> Ordinal n -> a-Sized xs %!! n = withListLikeF' xs $ LL.index xs (ordToInt n)+(%!!) :: (HasOrdinal nat, LL.ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c+Sized xs %!! n = LL.index xs $ P.fromIntegral $ ordToInt n {-# INLINE (%!!) #-}+{-# SPECIALISE (%!!) :: Sized [] (n :: TL.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: Sized [] (n :: Peano.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: Sized V.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: Sized V.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: TL.Nat) a -> Ordinal n -> a #-}+{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: Peano.Nat) a -> Ordinal n -> a #-} -- | Flipped version of '!!'.--- +-- -- Since 0.1.0.0-index :: (ListLikeF f) => Int -> Sized f (S m) c -> c-index = flip (!!)+index :: (ListLike (f a) a) => Int -> Sized f (Succ m) a -> a+index n (Sized xs) = LL.index xs n {-# INLINE index #-} -- | Flipped version of '%!!'.--- +-- -- Since 0.1.0.0-sIndex :: ListLikeF f => Ordinal n -> Sized f n c -> c+sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c sIndex = flip (%!!) {-# INLINE sIndex #-} -- | Take the first element of non-empty sequence. -- If you want to make case-analysis for general sequence, -- see <#ViewsAndPatterns Views and Patterns> section.--- +-- -- Since 0.1.0.0-head :: ListLikeF f => Sized f (S n) a -> a-head = givenListLikeF LL.head . runSized+head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat :< n) ~ 'True) => Sized f n a -> b+head = LL.head . runSized {-# INLINE head #-} -- | Take the last element of non-empty sequence. -- If you want to make case-analysis for general sequence, -- see <#ViewsAndPatterns Views and Patterns> section.--- +-- -- Since 0.1.0.0-last :: ListLikeF f => Sized f (S n) a -> a-last = givenListLikeF LL.last . runSized+last :: (HasOrdinal nat, (Zero nat :< n) ~ 'True, ListLike (f a) b) => Sized f n a -> b+last = LL.last . runSized {-# INLINE last #-} -- | Take the 'head' and 'tail' of non-empty sequence. -- If you want to make case-analysis for general sequence, -- see <#ViewsAndPatterns Views and Patterns> section.--- +-- -- Since 0.1.0.0-uncons :: ListLikeF f => Sized f (S n) a -> (a, Sized f n a)-uncons = givenListLikeF (\xs -> (LL.head xs, Sized $ LL.tail xs)) . runSized-{-# INLINE uncons #-}+uncons :: ListLike (f a) b => Sized f (Succ n) a -> (b, Sized f n a)+uncons = ((,) <$> LL.head <*> Sized . LL.tail) . runSized+{-# INLINE [1] uncons #-}+{-# RULES+"uncons/[]" [~1] forall (x :: a) (xs:: [a]).+ uncons (Sized (x : xs)) = (x, Sized xs)+"uncons/Seq" [~1] forall (xs:: Seq.Seq a).+ uncons (Sized xs) =+ case Seq.viewl xs of { (x Seq.:< ys) -> (x, Sized ys)+ ; _ -> P.error "Empty seq with non-zero index!"+ }+ #-} +uncons' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (b, Sized f n a)+uncons' _ = uncons+{-# INLINE uncons' #-}+ -- | Take the 'init' and 'last' of non-empty sequence. -- If you want to make case-analysis for general sequence, -- see <#ViewsAndPatterns Views and Patterns> section.--- +-- -- Since 0.1.0.0-unsnoc :: ListLikeF f => Sized f (S n) a -> (Sized f n a, a)-unsnoc = givenListLikeF (\xs -> (Sized $ LL.init xs, LL.last xs)) . runSized-{-# INLINE unsnoc #-}+unsnoc :: ListLike (f a) b => Sized f (Succ n) a -> (Sized f n a, b)+unsnoc = ((,) <$> Sized . LL.init <*> LL.last) . runSized+{-# NOINLINE [1] unsnoc #-}+{-# RULES+"unsnoc/Seq" [~1] forall (xs:: Seq.Seq a).+ unsnoc (Sized xs) =+ case Seq.viewr xs of { (ys Seq.:> x) -> (Sized ys, x)+ ; _ -> P.error "Empty seq with non-zero index!"+ }+ #-} +unsnoc' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (Sized f n a, b)+unsnoc' _ = unsnoc+{-# INLINE unsnoc' #-}++ -------------------------------------------------------------------------------- --- Slicing --------------------------------------------------------------------------------@@ -216,63 +301,63 @@ -- | Take the tail of non-empty sequence. -- If you want to make case-analysis for general sequence, -- see <#ViewsAndPatterns Views and Patterns> section.--- +-- -- Since 0.1.0.0-tail :: ListLikeF f => Sized f (S n) a -> Sized f n a-tail = givenListLikeF (Sized . LL.tail) . runSized+tail :: (HasOrdinal nat, ListLike (f a) a)=> Sized f (Succ n) a -> Sized f (n :: nat) a+tail = Sized . LL.tail . runSized {-# INLINE tail #-} -- | Take the initial segment of non-empty sequence. -- If you want to make case-analysis for general sequence, -- see <#ViewsAndPatterns Views and Patterns> section.--- +-- -- Since 0.1.0.0-init :: ListLikeF f => Sized f (S n) a -> Sized f n a-init = Sized . givenListLikeF LL.init . runSized+init :: ListLike (f a) a => Sized f (Succ n) a -> Sized f n a+init = Sized . LL.init . runSized {-# INLINE init #-} -- | @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 sn = Sized . givenListLikeF' (LL.take (sNatToInt sn))+take :: (ListLike (f a) a, (n :<= m) ~ 'True, HasOrdinal nat)+ => Sing (n :: nat) -> Sized f m a -> Sized f n a+take sn = Sized . LL.genericTake (demote' sn) . runSized {-# INLINE take #-} -- | @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-takeAtMost sn = givenListLikeF' $ Sized . LL.take (sNatToInt sn)+takeAtMost :: (ListLike (f a) a, HasOrdinal nat)+ => Sing (n :: nat) -> Sized f m a -> Sized f (Min n m) a+takeAtMost sn = Sized . LL.genericTake (demote $ Monomorphic sn) . runSized {-# INLINE takeAtMost #-} -- | @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-drop sn = givenListLikeF' $ Sized . LL.drop (sNatToInt sn)+drop :: (HasOrdinal nat, ListLike (f a) a, (n :<= m) ~ 'True)+ => Sing (n :: nat) -> Sized f m a -> Sized f (m :- n) a+drop sn = Sized . LL.genericDrop (demote' sn) . runSized {-# INLINE drop #-} -- | @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)-splitAt n = givenListLikeF' $ \xs ->- let (as, bs) = LL.splitAt (sNatToInt n) xs+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 n (Sized xs) =+ let (as, bs) = LL.genericSplitAt (demote' n) xs in (Sized as, Sized bs) {-# INLINE splitAt #-} @@ -280,12 +365,12 @@ -- 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)-splitAtMost n = givenListLikeF' $ \xs ->- let (as, bs) = LL.splitAt (sNatToInt n) xs+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 n (Sized xs) =+ let (as, bs) = LL.genericSplitAt (demote' n) xs in (Sized as, Sized bs) {-# INLINE splitAtMost #-} @@ -299,41 +384,42 @@ -------------------------------------------------------------------------------- -- | Empty sequence.--- +-- -- Since 0.1.0.0-empty :: forall f a. ListLikeF f => Sized f Z a-empty = withListLikeF (Proxy :: Proxy (f a)) $ Sized LL.empty+empty :: forall f a. (HasOrdinal nat, ListLike (f a) a) => Sized f (Zero nat :: nat) a+empty = Sized LL.empty {-# INLINE empty #-} -- | Sequence with one element.--- +-- -- Since 0.1.0.0-singleton :: forall f a. ListLikeF f => a -> Sized f One a-singleton = withListLikeF (Proxy :: Proxy (f a)) $ Sized . LL.singleton+singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a+singleton = Sized . LL.singleton {-# INLINE singleton #-} -- | 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 :: forall f a. ListLikeF f => f a -> SomeSized f a-toSomeSized = givenListLikeF $ \xs ->- case promote $ LL.length xs of+toSomeSized :: forall nat f a. (HasOrdinal nat, ListLike (f a) a)+ => f a -> SomeSized f nat a+toSomeSized = \xs ->+ case promote $ LL.genericLength xs of Monomorphic sn -> withSingI sn $ SomeSized sn $ unsafeToSized sn xs -- | Replicates the same value.--- +-- -- Since 0.1.0.0-replicate :: forall f n a. ListLikeF f => SNat n -> a -> Sized f n a-replicate sn a = withListLikeF (Proxy :: Proxy (f a)) $- Sized $ LL.replicate (sNatToInt sn) a+replicate :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a)+ => Sing n -> a -> Sized f n a+replicate sn a = Sized $ LL.genericReplicate (demote $ Monomorphic sn) a {-# INLINE replicate #-} -- | 'replicate' with the length inferred.--- +-- -- Since 0.1.0.0-replicate' :: (SingI (n :: Nat), ListLikeF f) => a -> Sized f n a+replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a replicate' = withSing replicate {-# INLINE replicate' #-} @@ -342,115 +428,107 @@ -------------------------------------------------------------------------------- -- | 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-cons a = givenListLikeF' $ Sized . LL.cons a+cons :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a+cons a = Sized . LL.cons a . runSized {-# INLINE cons #-} -- | Infix version of 'cons'.--- +-- -- Since 0.1.0.0-(<|) :: (ListLikeF f) => a -> Sized f n a -> Sized f (S n) a+(<|) :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a (<|) = cons {-# INLINE (<|) #-} infixr 5 <| -- | 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-snoc (Sized xs) a = withListLikeF' xs $ Sized $ LL.snoc xs a+snoc :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a+snoc (Sized xs) a = Sized $ LL.snoc xs a {-# INLINE snoc #-} -- | Infix version of 'snoc'.--- +-- -- Since 0.1.0.0-(|>) :: (ListLikeF f) => Sized f n a -> a -> Sized f (S n) a+(|>) :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a (|>) = snoc {-# INLINE (|>) #-} infixl 5 |> -- | Append two lists.--- +-- -- Since 0.1.0.0-append :: ListLikeF f => Sized f n a -> Sized f m a -> Sized f (n :+ m) a-append (Sized xs) (Sized ys) = withListLikeF' xs $ Sized $ LL.append xs ys+append :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n :+ m) a+append (Sized xs) (Sized ys) = Sized $ LL.append xs ys {-# INLINE append #-} -- | Infix version of 'append'.--- +-- -- Since 0.1.0.0-(++) :: (ListLikeF f) => Sized f n a -> Sized f m a -> Sized f (n :+ m) a+(++) :: (ListLike (f a) a) => Sized f n a -> Sized f m a -> Sized f (n :+ m) a (++) = append infixr 5 ++ -- | Concatenates multiple sequences into one.--- +-- -- Since 0.1.0.0-concat :: forall f f' m n a. (ListLikeF f, ListLikeF f')+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-concat =- givenListLikeF' $ withListLikeF (Proxy :: Proxy (f' (f a))) $- withListLikeF (Proxy :: Proxy (f a)) $- Sized . LL.concat . fmap runSized+concat = Sized . F.foldr LL.append LL.empty . P.fmap runSized+{-# INLINE [2] concat #-} +{-# RULES+"concat/list-list" [~1] forall (xss :: [Sized [] n a]).+ concat (Sized xss) = Sized (L.concatMap runSized xss)+"concat/list-list" [~2] forall (xss :: (ListLike (f a) a, ListLike (f (Sized f n a)) (Sized f n a))+ => f (Sized f n a)).+ concat (Sized xss) = Sized (LL.concatMap runSized xss)+ #-}+ -------------------------------------------------------------------------------- --- Zips -------------------------------------------------------------------------------- -- | Zipping two sequences. Length is adjusted to shorter one.--- +-- -- Since 0.1.0.0-zip :: forall f a b n m. (ListLikeF f)+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)-zip (Sized xs) (Sized ys) =- withListLikeF' ys $ withListLikeF' xs $- withListLikeF (Proxy :: Proxy (f (a,b))) $ Sized $- LL.zip xs ys+zip (Sized xs) (Sized ys) = Sized $ LL.zip xs ys {-# INLINE zip #-} -- | 'zip' for the sequences of the same length.--- +-- -- Since 0.1.0.0-zipSame :: forall f n a b. (ListLikeF f)+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)-zipSame (Sized xs) (Sized ys) =- withListLikeF' xs $ withListLikeF' ys $- withListLikeF (Proxy :: Proxy (f (a, b))) $- Sized $ LL.zip xs ys+zipSame (Sized xs) (Sized ys) = Sized $ LL.zip xs ys {-# INLINE zipSame #-} -- | Zipping two sequences with funtion. Length is adjusted to shorter one.--- +-- -- Since 0.1.0.0-zipWith :: forall f a b c m n. (ListLikeF f)+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-zipWith f (Sized xs) (Sized ys) =- withListLikeF' xs $ withListLikeF' ys $- withListLikeF (Proxy :: Proxy (f c)) $- Sized $ LL.zipWith f xs ys+zipWith f (Sized xs) (Sized ys) = Sized $ LL.zipWith f xs ys {-# INLINE zipWith #-} -- | 'zipWith' for the sequences of the same length.--- +-- -- Since 0.1.0.0-zipWithSame :: forall f a b c n. ListLikeF f+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-zipWithSame f (Sized xs) (Sized ys) =- withListLikeF' xs $ withListLikeF' ys $- withListLikeF (Proxy :: Proxy (f c)) $- Sized $ LL.zipWith f xs ys+zipWithSame f (Sized xs) (Sized ys) = Sized $ LL.zipWith f xs ys {-# INLINE zipWithSame #-} -- | Unzipping the sequence of tuples.--- +-- -- Since 0.1.0.0-unzip :: forall f n a b. (ListLikeF f)+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)-unzip (Sized xys) = withListLikeF' xys $- withListLikeF (Proxy :: Proxy (f b)) $- withListLikeF (Proxy :: Proxy (f a)) $+unzip (Sized xys) = let (xs, ys) = LL.unzip xys in (Sized xs, Sized ys) {-# INLINE unzip #-}@@ -461,56 +539,60 @@ -------------------------------------------------------------------------------- -- | Map function.--- +-- -- Since 0.1.0.0-map :: Functor f => (a -> b) -> Sized f n a -> Sized f n b-map f = Sized . fmap f . runSized+map :: (ListLike (f a) a, ListLike (f b) b) => (a -> b) -> Sized f n a -> Sized f n b+map f = Sized . LL.map f . runSized {-# INLINE map #-} +fmap :: forall f n a b. Functor f => (a -> b) -> Sized f n a -> Sized f n b+fmap f = Sized . P.fmap f . runSized+{-# INLINE fmap #-}+ -- | Reverse function.--- +-- -- Since 0.1.0.0-reverse :: ListLikeF f => Sized f n a -> Sized f n a-reverse = Sized . givenListLikeF LL.reverse . runSized+reverse :: ListLike (f a) a => Sized f n a -> Sized f n a+reverse = Sized . LL.reverse . runSized {-# INLINE reverse #-} -- | Intersperces.--- +-- -- Since 0.1.0.0-intersperse :: ListLikeF f => a -> Sized f n a -> Sized f ((Two :* n) :-: One) a-intersperse a = Sized . givenListLikeF' (LL.intersperse a)+intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 :* n) :-. 1) a+intersperse a = Sized . LL.intersperse a . runSized {-# INLINE intersperse #-} -- | Remove all duplicates.--- +-- -- Since 0.1.0.0-nub :: (ListLikeF f, Eq a) => Sized f n a -> SomeSized f a-nub = givenListLikeF' $ toSomeSized . LL.nub+nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a+nub = toSomeSized . LL.nub . runSized -- | Sorting sequence by ascending order.--- +-- -- Since 0.1.0.0-sort :: (ListLikeF f, Ord a)+sort :: (ListLike (f a) a, Ord a) => Sized f n a -> Sized f n a-sort = givenListLikeF' $ Sized . LL.sort+sort = Sized . LL.sort . runSized -- | Generalized version of 'sort'.--- +-- -- Since 0.1.0.0-sortBy :: (ListLikeF f) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a-sortBy cmp = givenListLikeF' $ Sized . LL.sortBy cmp+sortBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a+sortBy cmp = Sized . LL.sortBy cmp . runSized -- | 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-insert a = givenListLikeF' $ Sized . LL.insert a+insert :: (ListLike (f a) a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a+insert a = Sized . LL.insert a . runSized -- | 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-insertBy cmp a = givenListLikeF' $ Sized . LL.insertBy cmp a+insertBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a+insertBy cmp a = Sized . LL.insertBy cmp a . runSized --------------------------------------------------------------------------------@@ -522,80 +604,68 @@ -------------------------------------------------------------------------------- -- | Convert to list.--- +-- -- Since 0.1.0.0-toList :: ListLikeF f => Sized f n a -> [a]-toList = givenListLikeF LL.toList . runSized+toList :: ListLike (f a) a => Sized f n a -> [a]+toList = LL.toList . runSized {-# INLINE [2] toList #-} {-# RULES "toList/" forall (xs :: Sized [] a n).- toList xs = runSized xs+ Data.Sized.toList xs = runSized xs #-} -- | 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 :: forall f n a. ListLikeF f => SNat n -> [a] -> Maybe (Sized f n a)-fromList SZ _ = withListLikeF (Proxy :: Proxy (f a)) $- Just $ Sized (LL.empty :: f a)+fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a)+ => Sing (n :: nat) -> [a] -> Maybe (Sized f n a)+fromList Zero _ = Just $ Sized (LL.empty :: f a) fromList sn xs =- let len = sNatToInt sn+ let len = P.fromIntegral $ demote $ Monomorphic sn in if P.length xs < len then Nothing else Just $ unsafeFromList sn $ P.take len xs {-# INLINABLE [2] fromList #-} -{-# RULES-"fromList/List" forall sn (xs :: [a]).- fromList sn xs = toSized sn xs- #-}- -- | 'fromList' with the result length inferred.--- +-- -- Since 0.1.0.0-fromList' :: (ListLikeF f, SingI (n :: Nat)) => [a] -> Maybe (Sized f n a)+fromList' :: (ListLike (f a) a, SingI (n :: TL.Nat)) => [a] -> Maybe (Sized f n a) fromList' = withSing fromList {-# INLINE fromList' #-} --- | Unsafe version of 'fromList'. If the length of the given list does not +-- | 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 :: forall f n a. ListLikeF f => SNat n -> [a] -> Sized f n a-unsafeFromList _ xs =- withListLikeF (Proxy :: Proxy (f a)) $- Sized $ LL.fromList xs+unsafeFromList :: forall f n a. ListLike (f a) a => Sing n -> [a] -> Sized f n a+unsafeFromList _ xs = Sized $ LL.fromList xs {-# INLINE [2] unsafeFromList #-} -{-# RULES-"unsafeFromList/List" forall sn (xs :: [a]).- unsafeFromList sn xs = Sized (P.take (sNatToInt sn) xs)- #-}- -- | 'unsafeFromList' with the result length inferred.--- +-- -- Since 0.1.0.0-unsafeFromList' :: (SingI (n :: Nat), ListLikeF f) => [a] -> Sized f n a+unsafeFromList' :: (SingI (n :: TL.Nat), ListLike (f a) a) => [a] -> Sized f n a unsafeFromList' = withSing unsafeFromList {-# INLINE unsafeFromList' #-} -- | Construct a @Sized f n a@ by padding default value if the given list is short.--- +-- -- Since 0.1.0.0-fromListWithDefault :: forall f n a. ListLikeF f => SNat n -> a -> [a] -> Sized f n a+fromListWithDefault :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a)+ => Sing n -> a -> [a] -> Sized f n a fromListWithDefault sn def xs =- let len = sNatToInt sn- in withListLikeF (Proxy :: Proxy (f a)) $- Sized $ LL.fromList (P.take len xs) `LL.append` LL.replicate (len - P.length xs) def+ let len = demote' sn+ in Sized $ LL.fromList (L.genericTake len xs) `LL.append` LL.genericReplicate (len - L.genericLength xs) def {-# INLINABLE fromListWithDefault #-} -- | 'fromListWithDefault' with the result length inferred.--- +-- -- Since 0.1.0.0-fromListWithDefault' :: (SingI (n :: Nat), ListLikeF f) => a -> [a] -> Sized f n a+fromListWithDefault' :: (SingI (n :: TL.Nat), ListLike (f a) a) => a -> [a] -> Sized f n a fromListWithDefault' = withSing fromListWithDefault {-# INLINE fromListWithDefault' #-} @@ -604,7 +674,7 @@ -------------------------------------------------------------------------------- -- | Forget the length and obtain the wrapped base container.--- +-- -- Since 0.1.0.0 unsized :: Sized f n a -> f a unsized = runSized@@ -613,51 +683,53 @@ -- | 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 sn = givenListLikeF $ \xs ->- let len = sNatToInt sn- in if LL.length xs < len+toSized :: (HasOrdinal nat, ListLike (f a) a)+ => Sing (n :: nat) -> f a -> Maybe (Sized f n a)+toSized sn xs =+ let len = demote' sn+ in if LL.genericLength xs < len then Nothing- else Just $ unsafeToSized sn $ LL.take len xs+ else Just $ unsafeToSized sn $ LL.genericTake len xs {-# INLINABLE [2] toSized #-} -- | 'toSized' with the result length inferred.--- +-- -- Since 0.1.0.0-toSized' :: (ListLikeF f, SingI (n :: Nat)) => f a -> Maybe (Sized f n a)+toSized' :: (ListLike (f a) a, SingI (n :: TL.Nat)) => f a -> Maybe (Sized f n a) toSized' = withSing toSized {-# INLINE toSized' #-} --- | Unsafe version of 'toSized'. If the length of the given list does not +-- | 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 :: Sing n -> f a -> Sized f n a unsafeToSized _ = Sized {-# INLINE [2] unsafeToSized #-} -- | 'unsafeToSized' with the result length inferred.--- +-- -- Since 0.1.0.0-unsafeToSized' :: (SingI (n :: Nat), ListLikeF f) => f a -> Sized f n a+unsafeToSized' :: (SingI (n :: TL.Nat), ListLike (f a) a) => f a -> Sized f n a unsafeToSized' = withSing unsafeToSized {-# INLINE unsafeToSized' #-} -- | 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 sn def = givenListLikeF $ \xs ->- let len = sNatToInt sn+toSizedWithDefault :: (HasOrdinal nat, ListLike (f a) a)+ => Sing (n :: nat) -> a -> f a -> Sized f n a+toSizedWithDefault sn def xs =+ let len = P.fromIntegral $ demote (Monomorphic sn) in Sized $ LL.take len xs `LL.append` LL.replicate (len - LL.length xs) def {-# INLINABLE toSizedWithDefault #-} -- | 'toSizedWithDefault' with the result length inferred.--- +-- -- Since 0.1.0.0-toSizedWithDefault' :: (SingI (n :: Nat), ListLikeF f) => a -> f a -> Sized f n a+toSizedWithDefault' :: (SingI (n :: TL.Nat), ListLike (f a) a) => a -> f a -> Sized f n a toSizedWithDefault' = withSing toSizedWithDefault {-# INLINE toSizedWithDefault' #-} @@ -672,76 +744,76 @@ -- | 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 data Partitioned f n a where- Partitioned :: (ListLikeF f, SingI n, SingI m)- => SNat n- -> Sized f (n :: Nat) a- -> SNat m- -> Sized f (m :: Nat) a+ Partitioned :: (ListLike (f a) a)+ => Sing n+ -> Sized f (n :: TL.Nat) a+ -> Sing m+ -> Sized f (m :: TL.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-takeWhile p = givenListLikeF' $ toSomeSized . LL.takeWhile p+takeWhile :: (HasOrdinal nat, ListLike (f a) a)+ => (a -> Bool) -> Sized f n a -> SomeSized f nat a+takeWhile p = toSomeSized . LL.takeWhile p . runSized {-# INLINE takeWhile #-} -- | 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-dropWhile p = givenListLikeF' $ toSomeSized . LL.dropWhile p+dropWhile :: (HasOrdinal nat, ListLike (f a) a)+ => (a -> Bool) -> Sized f n a -> SomeSized f nat a+dropWhile p = toSomeSized . LL.dropWhile p . runSized {-# INLINE dropWhile #-} -- | 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+span :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a-span p = givenListLikeF' $ \xs ->- let (as, bs) = LL.span p xs- in case (toSomeSized as, toSomeSized bs) of- (SomeSized lenL ls, SomeSized lenR rs) ->- unsafeCoerce $ Partitioned lenL ls lenR rs+span p xs =+ let (as, bs) = LL.span p $ runSized xs+ in case (toSomeSized as, toSomeSized bs) of+ (SomeSized lenL ls, SomeSized lenR rs) ->+ unsafeCoerce $ Partitioned lenL ls lenR rs {-# INLINE span #-} -- | 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+break :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a-break p = givenListLikeF' $ \xs ->- let (as, bs) = LL.break p xs- in case (toSomeSized as, toSomeSized bs) of- (SomeSized lenL ls, SomeSized lenR rs) ->- unsafeCoerce $ Partitioned lenL ls lenR rs+break p (Sized xs) =+ let (as, bs) = LL.break p xs+ in case (toSomeSized as, toSomeSized bs) of+ (SomeSized lenL ls, SomeSized lenR rs) ->+ unsafeCoerce $ Partitioned lenL ls lenR rs {-# INLINE break #-} -- | 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+partition :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a-partition p = givenListLikeF' $ \xs ->+partition p (Sized xs) = let (as, bs) = LL.partition p xs in case (toSomeSized as, toSomeSized bs) of (SomeSized lenL ls, SomeSized lenR rs) ->@@ -752,82 +824,170 @@ --- Searching -------------------------------------------------------------------------------- -- | Membership test; see also 'notElem'.--- +-- -- Since 0.1.0.0-elem :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool-elem a = givenListLikeF' $ LL.elem a+elem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool+elem a = LL.elem a . runSized {-# INLINE elem #-} -- | Negation of 'elem'.--- +-- -- Since 0.1.0.0-notElem :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool-notElem a = givenListLikeF' $ LL.notElem a+notElem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool+notElem a = LL.notElem a . runSized {-# INLINE notElem #-} -- | Find the element satisfying the predicate.--- +-- -- Since 0.1.0.0-find :: ListLikeF f => (a -> Bool) -> Sized f n a -> Maybe a-find p = givenListLikeF' $ LL.find p-{-# INLINE find #-}+find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a+find p = F.find p+{-# INLINE[1] find #-}+{-# RULES+"find/List" [~1] forall p (xs :: [a]).+ find p (Sized xs) = L.find p xs+"find/Vector" [~1] forall p xs.+ find p (Sized xs) = V.find p xs+"find/Storable Vector" [~1] forall p (xs :: SV.Storable a => SV.Vector a).+ find p (Sized xs) = SV.find p xs+"find/Unboxed Vector" [~1] forall p (xs :: UV.Unbox a => UV.Vector a).+ find p (Sized xs) = UV.find p xs+ #-} +-- | @'Foldable'@ version of @'find'@.+findF :: (Foldable f) => (a -> Bool) -> Sized f n a -> Maybe a+findF p = getFirst. F.foldMap (\a -> if p a then First (Just a) else First Nothing) . runSized+{-# INLINE [1] findF #-}+{-# SPECIALISE [0] findF :: (a -> Bool) -> Sized Seq.Seq n a -> Maybe a #-}+{-# RULES+"findF/list" [~1] forall p.+ findF p = L.find p+ #-}+ -- | @'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-findIndex p = givenListLikeF' $ LL.findIndex p+findIndex :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Maybe Int+findIndex p = LL.findIndex p . runSized {-# INLINE findIndex #-} -- | 'Ordinal' version of 'findIndex'.--- +-- -- Since 0.1.0.0-sFindIndex :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)-sFindIndex p = fmap toEnum . findIndex p+sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat)+ => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)+sFindIndex p = P.fmap toEnum . findIndex p {-# INLINE sFindIndex #-} +-- | @'findIndex'@ implemented in terms of @'FoldableWithIndex'@+findIndexIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> Maybe i+findIndexIF p = P.fmap fst . ifind (P.const p) . runSized+{-# INLINE [1] findIndexIF #-}+{-# RULES+"findIndexIF/list" [~1] forall p.+ findIndexIF p = L.findIndex p . runSized+"findIndexIF/vector" [~1] forall p.+ findIndexIF p = V.findIndex p . runSized+ #-}++-- | @'sFindIndex'@ implemented in terms of @'FoldableWithIndex'@+sFindIndexIF :: (FoldableWithIndex i f, P.Integral i, HasOrdinal nat, SingI n)+ => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n)+sFindIndexIF p = P.fmap fst . ifind (P.const p)+{-# INLINE [1] sFindIndexIF #-}+-- {-# RULES+-- "sFindIndexIF/list" [~1] forall p .+-- sFindIndexIF p = P.fmap toEnum . L.findIndex p . runSized+-- "sFindIndexIF/vector" [~1] forall p.+-- sFindIndexIF p = P.fmap toEnum . V.findIndex p . runSized+-- #-}+ -- | @'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]-findIndices p = givenListLikeF' $ LL.findIndices p+findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int]+findIndices p = LL.findIndices p . runSized {-# INLINE findIndices #-}+{-# SPECIALISE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-} +-- | @'findIndices'@ implemented in terms of @'FoldableWithIndex'@+findIndicesIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> [i]+findIndicesIF p = flip appEndo [] . ifoldMap (\i x -> if p x then Endo (i:) else Endo P.id) . runSized+{-# INLINE [1] findIndicesIF #-}+{-# RULES+"findIndicesIF/list" [~1] forall p.+ findIndicesIF p = L.findIndices p . runSized+"findIndicesIF/vector" [~1] forall p.+ findIndicesIF p = V.toList . V.findIndices p . runSized+ #-}++ -- | 'Ordinal' version of 'findIndices'.--- +-- -- Since 0.1.0.0-sFindIndices :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> [Ordinal n]-sFindIndices p = fmap toEnum . findIndices p+sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a)+ => (a -> Bool) -> Sized f n a -> [Ordinal n]+sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p {-# INLINE sFindIndices #-} +sFindIndicesIF :: (FoldableWithIndex i f, P.Integral i, HasOrdinal nat, SingI n)+ => (a -> Bool) -> Sized f (n :: nat) a -> [Ordinal n]+sFindIndicesIF p = flip appEndo [] .+ ifoldMap (\i x -> if p x then Endo (P.toEnum (P.fromIntegral i):) else Endo P.id) .+ runSized+{-# INLINE [1] sFindIndicesIF #-}+-- {-# RULES+-- "sFindIndicesIF/list" [~1] forall p.+-- sFindIndicesIF p = P.map toEnum . L.findIndices p . runSized+-- "sFindIndicesIF/vector" [~1] forall p.+-- sFindIndicesIF p = V.toList . V.map toEnum . V.findIndices p . runSized+-- #-}+ -- | 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-elemIndex a = findIndex (== a)+elemIndex :: (Eq a, ListLike (f a) a) => a -> Sized f n a -> Maybe Int+elemIndex a (Sized xs) = LL.elemIndex a xs {-# INLINE elemIndex #-} -- | Ordinal version of 'elemIndex'--- --- Since 0.1.0.0-sElemIndex :: (SingI n, ListLikeF f, Eq a)+-- 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+sElemIndex :: forall (n :: nat) f a.+ (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) => a -> Sized f n a -> Maybe (Ordinal n)-sElemIndex a = sFindIndex (== a)+sElemIndex a (Sized xs) = do+ i <- LL.elemIndex a xs+ case promote (P.fromIntegral i) of+ Monomorphic sn ->+ case sn %:< (sing :: Sing n) of+ STrue -> Just (OLt sn)+ SFalse -> Nothing {-# INLINE sElemIndex #-} +sUnsafeElemIndex :: forall (n :: nat) f a.+ (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat)+ => a -> Sized f n a -> Maybe (Ordinal n)+sUnsafeElemIndex a (Sized xs) =+ unsafeFromInt . P.fromIntegral <$> LL.elemIndex a xs -- | 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]-elemIndices a = givenListLikeF' $ LL.elemIndices a+elemIndices :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> [Int]+elemIndices a = LL.elemIndices a . runSized {-# INLINE elemIndices #-} -- | Ordinal version of 'elemIndices'--- +-- -- Since 0.1.0.0-sElemIndices :: (SingI n, ListLikeF f, Eq a) => a -> Sized f n a -> [Ordinal n]-sElemIndices p = fmap toEnum . elemIndices p+sElemIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a, Eq a)+ => a -> Sized f n a -> [Ordinal n]+sElemIndices p = P.fmap (unsafeFromInt . P.fromIntegral) . elemIndices p {-# INLINE sElemIndices #-} --------------------------------------------------------------------------------@@ -847,64 +1007,65 @@ {-$views #views# With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows:- + @-slen :: ('SingI' n, 'ListLikeF' f) => 'Sized' f n a -> 'SNat' n+slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n slen ('viewCons' -> 'NilCV') = 'SZ' slen ('viewCons' -> _ '::-' as) = 'SS' (slen as) slen _ = error "impossible" @- - The constraint @('SingI' n, 'ListLikeF' f)@ is needed for view function.++ The constraint @('SingI' n, 'ListLike (f a) a' f)@ is needed for view function. In the above, we have extra wildcard pattern (@_@) at the last. Code compiles if we removed it, but current GHC warns for incomplete pattern, although we know first two patterns exhausts all the case.- + Equivalently, we can use snoc-style pattern-matching:- + @-slen :: ('SingI' n, 'ListLikeF' f) => 'Sized' f n a -> 'SNat' n+slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n slen ('viewSnoc' -> 'NilSV') = 'SZ' slen ('viewSnoc' -> as ':-::' _) = 'SS' (slen as) @ -} -- | View of the left end of sequence (cons-side).--- +-- -- Since 0.1.0.0 data ConsView f n a where- NilCV :: ConsView f Z a- (::-) :: SingI n => a -> Sized f n a -> ConsView f (S n) a+ NilCV :: ConsView f (Zero nat) a+ (::-) :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a infixr 5 ::- -- | Case analysis for the cons-side of sequence.--- +-- -- Since 0.1.0.0-viewCons :: forall f a n. (SingI n, ListLikeF f)+viewCons :: forall f a (n :: nat). (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> ConsView f n a-viewCons sz = case sing :: SNat n of- SZ -> NilCV- SS n' -> withSingI n' $ head sz ::- tail sz+viewCons sz = case zeroOrSucc (sLength sz) of+ IsZero -> NilCV+ IsSucc n' -> withSingI n' $ P.uncurry (::-) (uncons' n' sz) -- | View of the left end of sequence (snoc-side).--- +-- -- Since 0.1.0.0 data SnocView f n a where- NilSV :: SnocView f Z a- (:-::) :: SingI n => Sized f n a -> a -> SnocView f (S n) a+ NilSV :: SnocView f (Zero nat) a+ (:-::) :: SingI n => Sized f n a -> a -> SnocView f (Succ n) a infixl 5 :-:: -- | Case analysis for the snoc-side of sequence.--- +-- -- Since 0.1.0.0-viewSnoc :: forall f n a. (SingI n, ListLikeF f)+viewSnoc :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> SnocView f n a-viewSnoc sz = case sing :: SNat n of- SZ -> NilSV- SS n -> withSingI n $ init sz :-:: last sz+viewSnoc sz = case zeroOrSucc (sLength sz) of+ IsZero -> NilSV+ IsSucc n' ->+ withSingI n' $ P.uncurry (:-::) (unsnoc' n' sz) {-$patterns #patterns# @@ -912,27 +1073,27 @@ it is rather clumsy to nest it. For example: @-nextToHead :: ('ListLikeF' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a+nextToHead :: ('ListLike (f a) a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a nextToHead ('viewCons' -> _ '::-' ('viewCons' -> a '::-' _)) = a @ In such a case, with @PatternSynonyms@ extension we can write as follows: @-nextToHead :: ('ListLikeF' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a+nextToHead :: ('ListLike (f a) a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a nextToHead (_ ':<' a ':<' _) = a @ Of course, we can also rewrite above @slen@ example using @PatternSynonyms@: @-slen :: ('SingI' n, 'ListLikeF' f) => 'Sized' f n a -> 'SNat' n+slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n slen 'NilL' = 'SZ' slen (_ ':<' as) = 'SS' (slen as) slen _ = error "impossible" @ - So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to + So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. @':<'@, @'NilL'@, @':>'@ and @'NilR'@ are neither functions nor data constructors, but pattern synonyms so we cannot use them in expression contexts.@@ -944,9 +1105,51 @@ infixr 5 :< -- | Pattern synonym for cons-side uncons.-pattern a :< b <- (viewCons -> a ::- b)-pattern NilL <- (viewCons -> NilCV)+pattern (:<) :: forall nat f (n :: nat) a.+ (ListLike (f a) a, HasOrdinal nat)+ => forall (n1 :: nat).+ (n ~ Succ n1, SingI n1)+ => a -> Sized f n1 a -> Sized f n a+pattern a :< as <- (viewCons -> a ::- as) where+ a :< as = a <| as +pattern NilL :: forall nat f (n :: nat) a.+ (ListLike (f a) a, HasOrdinal nat)+ => (n ~ Zero nat) => Sized f n a+pattern NilL <- (viewCons -> NilCV) where+ NilL = empty+ infixl 5 :>-pattern a :> b <- (viewSnoc -> a :-:: b)-pattern NilR <- (viewSnoc -> NilSV)++pattern (:>) :: forall nat f (n :: nat) a.+ (ListLike (f a) a, HasOrdinal nat)+ => forall (n1 :: nat).+ (n ~ Succ n1, SingI n1)+ => Sized f n1 a -> a -> Sized f n a+pattern a :> b <- (viewSnoc -> a :-:: b) where+ a :> b = a |> b++pattern NilR :: forall nat f (n :: nat) a.+ (ListLike (f a) a, HasOrdinal nat)+ => n ~ Zero nat => Sized f n a+pattern NilR <- (viewSnoc -> NilSV) where+ NilR = empty++-- | Applicative instance, generalizing @'Data.Monoid.ZipList'@.+instance (Functor f, HasOrdinal nat, SingI n, ListLikeF f)+ => P.Applicative (Sized f (n :: nat)) where+ {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized [] (n :: TL.Nat)) #-}+ {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized Seq.Seq (n :: TL.Nat)) #-}+ {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized V.Vector (n :: TL.Nat)) #-}++ pure (x :: a) =+ withListLikeF (Nothing :: Maybe (f a)) $+ replicate' x+ {-# INLINE pure #-}++ Sized (fs :: f (a -> b)) <*> Sized (xs :: f a) =+ withListLikeF (Nothing :: Maybe (f (a -> b))) $+ withListLikeF (Nothing :: Maybe (f a)) $+ withListLikeF (Nothing :: Maybe (f b)) $+ Sized $ LL.zipWith ($) fs xs+ {-# INLINE (<*>) #-}
+ Data/Sized/Builtin.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-}+{-# LANGUAGE ViewPatterns #-}+-- | This module exports @'S.Sized'@ type specialized to+-- GHC's built-in type numeral @'TL.Nat'@.+module Data.Sized.Builtin+ (Ordinal, Sized, module Data.Sized,+ pattern (:<), pattern NilL, pattern (:>), pattern NilR) where+import Data.Sized hiding ((:<), (:>), NilL, NilR, Sized)+import qualified Data.Sized as S++import Data.ListLike (ListLike)+import Data.Singletons.Prelude (SingI)+import Data.Singletons.Prelude.Enum (PEnum (..))+import qualified Data.Type.Ordinal as O+import qualified GHC.TypeLits as TL++type Ordinal (n :: TL.Nat) = O.Ordinal n+type Sized f (n :: TL.Nat) = S.Sized f n++pattern (:<) :: forall f (n :: TL.Nat) a.+ (ListLike (f a) a)+ => forall (n1 :: TL.Nat).+ (n ~ Succ n1, SingI n1)+ => a -> Sized f n1 a -> Sized f n a+pattern a :< b = a S.:< b+infixr 5 :<++pattern NilL :: forall f (n :: TL.Nat) a.+ (ListLike (f a) a)+ => n ~ 0 => Sized f n a+pattern NilL = S.NilL++pattern (:>) :: forall f (n :: TL.Nat) a.+ (ListLike (f a) a)+ => forall (n1 :: TL.Nat).+ (n ~ Succ n1, SingI n1)+ => Sized f n1 a -> a -> Sized f n a+pattern a :> b = a S.:> b+infixl 5 :>++pattern NilR :: forall f (n :: TL.Nat) a.+ (ListLike (f a) a, SingI n)+ => n ~ 0 => Sized f n a+pattern NilR = S.NilR
+ Data/Sized/Flipped.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable, EmptyDataDecls, ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-}+{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PatternSynonyms #-}+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies, TypeInType #-}+{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns #-}+module Data.Sized.Flipped (Flipped(..),+ pattern (:<), pattern NilL,+ pattern (:>), pattern NilR) where+import qualified Data.Sized as Orig+import Data.Sized.Internal++import Control.DeepSeq (NFData(..))+import Control.Lens.At (Index, IxValue, Ixed (..))+import Control.Lens.TH (makeWrapped)+import Control.Lens.Wrapped (_Wrapped)+import Data.Hashable (Hashable (..))+import Data.Kind (Type)+import qualified Data.ListLike as LL+import Data.MonoTraversable (Element, MonoFoldable (..))+import Data.MonoTraversable (MonoFunctor (..))+import Data.MonoTraversable (MonoTraversable (..))+import qualified Data.Sequence as Seq+import Data.Singletons.Prelude.Enum (PEnum (..))+import qualified Data.Type.Natural as PN+import Data.Type.Natural.Class (Zero)+import Data.Type.Ordinal (HasOrdinal, Ordinal (..))+import Data.Typeable (Typeable)+import qualified Data.Vector as V+import qualified Data.Vector.Storable as SV+import qualified Data.Vector.Unboxed as UV+import qualified GHC.TypeLits as TL++-- | Wrapper for @'Sized'@ which takes length as its last element, instead of the second.+--+-- Since 0.2.0.0+newtype Flipped f a n = Flipped { runFlipped :: Sized f n a }+ deriving (Show, Eq, Ord, Typeable, NFData, Hashable)++makeWrapped ''Flipped++type instance Index (Flipped f a n) = Ordinal n+type instance IxValue (Flipped f a n) = IxValue (f a)+type instance Element (Flipped f a n) = Element (Sized f n a)+deriving instance MonoFunctor (f a) => MonoFunctor (Flipped f a n)+deriving instance MonoFoldable (f a) => MonoFoldable (Flipped f a n)+instance (MonoTraversable (f a)) => MonoTraversable (Flipped f a n) where+ otraverse = _Wrapped . otraverse+ {-# INLINE otraverse #-}++ omapM = _Wrapped . omapM+ {-# INLINE omapM #-}++instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat)+ => Ixed (Flipped f a (n :: nat)) where+ {-# SPECIALISE instance Ixed (Flipped [] a (n :: TL.Nat)) #-}+ {-# SPECIALISE instance Ixed (Flipped [] a (n :: PN.Nat)) #-}+ {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: TL.Nat)) #-}+ {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: PN.Nat)) #-}+ {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: PN.Nat)) #-}+ {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: TL.Nat)) #-}+ {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: PN.Nat)) #-}+ {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: TL.Nat)) #-}+ {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: PN.Nat)) #-}+ ix o = _Wrapped . ix o+ {-# INLINE ix #-}++pattern (:<) :: forall nat (f :: Type -> Type) (n :: nat) a.+ (LL.ListLike (f a) a, HasOrdinal nat)+ => forall (n1 :: nat). (n ~ Succ n1, PN.SingI n1)+ => a -> Flipped f a n1 -> Flipped f a n+pattern a :< as <- Flipped (a Orig.:< (Flipped -> as)) where+ a :< Flipped as = Flipped (a Orig.:< as)++pattern NilL :: forall nat (f :: Type -> Type) (n :: nat) a.+ (LL.ListLike (f a) a, HasOrdinal nat)+ => n ~ Zero nat => Flipped f a n+pattern NilL = Flipped Orig.NilL++pattern (:>) :: forall nat (f :: Type -> Type) (n :: nat) a.+ (LL.ListLike (f a) a, HasOrdinal nat)+ => forall (n1 :: nat). (n ~ Succ n1, PN.SingI n1)+ => Flipped f a n1 -> a -> Flipped f a n+pattern as :> a <- Flipped ((Flipped -> as) Orig.:> a) where+ Flipped as :> a = Flipped (as Orig.:> a)++pattern NilR :: forall nat (f :: Type -> Type) (n :: nat) a.+ (LL.ListLike (f a) a, HasOrdinal nat)+ => n ~ Zero nat => Flipped f a n+pattern NilR = Flipped Orig.NilR
Data/Sized/Internal.hs view
@@ -1,60 +1,183 @@ {-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFunctor #-}-{-# LANGUAGE DeriveTraversable, EmptyDataDecls, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, KindSignatures #-}+{-# LANGUAGE DeriveTraversable, EmptyDataDecls, ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-} {-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PolyKinds #-}-{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators #-}+{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeInType, TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Data.Sized.Internal- (Sized(..), instLL, instFunctor, ListLikeF,- withListLikeF, withListLikeF', givenListLikeF,- givenListLikeF') where-import Data.Constraint-import Data.Constraint.Forall (Forall, inst)-import Data.Foldable (Foldable)-import Data.ListLike (FoldableLL (..), ListLike)-import qualified Data.ListLike as LL-import Data.Proxy-import qualified Data.Sequence as Seq-import Data.Traversable (Traversable)-import Data.Type.Natural (Nat)-import Data.Typeable (Typeable)-import qualified Data.Vector as V+ (Sized(..),instLL, instFunctor, ListLikeF,+ withListLikeF, withListLikeF'+ ) where+import Control.DeepSeq (NFData (..))+import Control.Lens.At (Index, IxValue, Ixed (..))+import Control.Lens.Indexed (FoldableWithIndex (..))+import Control.Lens.Indexed (FunctorWithIndex (..))+import Control.Lens.Indexed (TraversableWithIndex (..))+import Data.Constraint ((:-) (..), (:=>) (..), Class (..))+import Data.Constraint (Dict (..), trans, weaken1, weaken2)+import Data.Constraint ((&&&), (\\))+import Data.Constraint.Forall (Forall, inst)+import Data.Foldable (Foldable)+import Data.Hashable (Hashable (..))+import Data.Kind (Type)+import Data.ListLike (ListLike)+import Data.MonoTraversable (Element, MonoFoldable (..))+import Data.MonoTraversable (MonoFunctor (..))+import Data.MonoTraversable (MonoTraversable (..))+import Data.Proxy (Proxy (..))+import qualified Data.Sequence as Seq+import Data.Singletons.Prelude (SingI)+import Data.Traversable (Traversable)+import qualified Data.Type.Natural as PN+import Data.Type.Ordinal (HasOrdinal, Ordinal (..), ordToInt)+import Data.Type.Ordinal (unsafeFromInt)+import Data.Typeable (Typeable)+import qualified Data.Vector as V+import qualified Data.Vector.Storable as SV+import qualified Data.Vector.Unboxed as UV+import qualified GHC.TypeLits as TL -- | @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-newtype Sized f (n :: Nat) a =+-- Since 0.2.0.0+newtype Sized (f :: Type -> Type) (n :: nat) a = Sized { runSized :: f a } deriving (Eq, Ord, Typeable, Functor, Foldable, Traversable) --- | Since 0.1.0.0-instance ListLikeF f => FoldableLL (Sized f n a) a where- {-# SPECIALISE instance LL.FoldableLL (Sized [] n a) a #-}- {-# SPECIALISE instance LL.FoldableLL (Sized V.Vector n a) a #-}- {-# SPECIALISE instance LL.FoldableLL (Sized Seq.Seq n a) a #-}- foldl f a = givenListLikeF' $ LL.foldl f a- {-# INLINE foldl #-}- foldl' f a = givenListLikeF' $ LL.foldl' f a- {-# INLINE foldl' #-}- foldl1 f = givenListLikeF' $ LL.foldl1 f- {-# INLINE foldl1 #-}- foldr f a = givenListLikeF' $ LL.foldr f a- {-# INLINE foldr #-}- foldr' f a = givenListLikeF' $ LL.foldr' f a- {-# INLINE foldr' #-}- foldr1 f = givenListLikeF' $ LL.foldr1 f- {-# INLINE foldr1 #-}+type instance Element (Sized f n a) = Element (f a) +-- | Since 0.2.0.0+deriving instance MonoFoldable (f a)+ => MonoFoldable (Sized f n a)++-- | Since 0.2.0.0+deriving instance MonoFunctor (f a)+ => MonoFunctor (Sized f n a)++-- | Since 0.2.0.0+instance {-# OVERLAPPABLE #-} (MonoTraversable (f a))+ => MonoTraversable (Sized f n a) where+ {-# SPECIALISE instance MonoTraversable (Sized [] n a) #-}+ {-# SPECIALISE instance MonoTraversable (Sized V.Vector n a) #-}+ {-# SPECIALISE instance MonoTraversable (Sized Seq.Seq n a) #-}+ {-# SPECIALISE instance UV.Unbox a => MonoTraversable (Sized UV.Vector n a) #-}+ {-# SPECIALISE instance SV.Storable a => MonoTraversable (Sized SV.Vector n a) #-}+ otraverse f = fmap Sized . otraverse f . runSized+ omapM f = fmap Sized . omapM f. runSized++-- | Since 0.2.0.0+instance {-# OVERLAPS #-} SV.Storable a => MonoTraversable (Sized SV.Vector n a) where+ otraverse f = fmap Sized . otraverse f . runSized+ omapM f = fmap Sized . omapM f . runSized++-- | Since 0.2.0.0+instance {-# OVERLAPS #-} UV.Unbox a => MonoTraversable (Sized UV.Vector n a) where+ otraverse f = fmap Sized . otraverse f . runSized+ omapM f = fmap Sized . omapM f . runSized++deriving instance NFData (f a) => NFData (Sized f n a)+deriving instance Hashable (f a) => Hashable (Sized f n a)+ instance Show (f a) => Show (Sized f n a) where showsPrec d (Sized x) = showsPrec d x++-- | Since 0.2.0.0+type instance Index (Sized f n a) = Ordinal n++-- | Since 0.2.0.0+type instance IxValue (Sized f n a) = IxValue (f a)+instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat)+ => Ixed (Sized f (n :: nat) a) where+ {-# SPECIALISE instance Ixed (Sized [] (n :: TL.Nat) a) #-}+ {-# SPECIALISE instance Ixed (Sized [] (n :: PN.Nat) a) #-}+ {-# SPECIALISE instance Ixed (Sized V.Vector (n :: TL.Nat) a) #-}+ {-# SPECIALISE instance Ixed (Sized V.Vector (n :: PN.Nat) a) #-}+ {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: TL.Nat) a) #-}+ {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: PN.Nat) a) #-}+ {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: TL.Nat) a) #-}+ {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: PN.Nat) a) #-}+ {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: TL.Nat) a) #-}+ {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: PN.Nat) a) #-}+ {-# INLINE ix #-}+ ix n f = fmap Sized . ix (fromIntegral $ ordToInt n) f . runSized++-- | Since 0.2.0.0+instance (Integral i, FunctorWithIndex i f, HasOrdinal nat, SingI n)+ => FunctorWithIndex (Ordinal (n :: nat)) (Sized f n) where+ imap f = Sized . imap (f . unsafeFromInt . fromIntegral) . runSized+ {-# INLINE imap #-}+ {-# SPECIALISE instance TL.KnownNat n+ => FunctorWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => FunctorWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-}+ {-# SPECIALISE instance TL.KnownNat n+ => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-}+ {-# SPECIALISE instance TL.KnownNat n+ => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-}++-- | Since 0.2.0.0+instance (Integral i, FoldableWithIndex i f, HasOrdinal nat, SingI n)+ => FoldableWithIndex (Ordinal (n :: nat)) (Sized f n) where+ ifoldMap f = ifoldMap (f . unsafeFromInt . fromIntegral) . runSized+ {-# INLINE ifoldMap #-}++ ifoldr f e = ifoldr (f . unsafeFromInt . fromIntegral) e . runSized+ {-# INLINE ifoldr #-}++ ifoldl f e = ifoldl (f . unsafeFromInt . fromIntegral) e . runSized+ {-# INLINE ifoldl #-}++ ifoldr' f e = ifoldr' (f . unsafeFromInt . fromIntegral) e . runSized+ {-# INLINE ifoldr' #-}++ ifoldl' f e = ifoldl' (f . unsafeFromInt . fromIntegral) e . runSized+ {-# INLINE ifoldl' #-}++ {-# SPECIALISE instance TL.KnownNat n+ => FoldableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => FoldableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-}+ {-# SPECIALISE instance TL.KnownNat n+ => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-}+ {-# SPECIALISE instance TL.KnownNat n+ => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-}++-- | Since 0.2.0.0+instance (Integral i, TraversableWithIndex i f, HasOrdinal nat, SingI n)+ => TraversableWithIndex (Ordinal (n :: nat)) (Sized f n) where+ itraverse f = fmap Sized . itraverse (f . unsafeFromInt . fromIntegral) . runSized+ {-# INLINE itraverse #-}++ {-# SPECIALISE instance TL.KnownNat n+ => TraversableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => TraversableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-}+ {-# SPECIALISE instance TL.KnownNat n+ => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-}+ {-# SPECIALISE instance TL.KnownNat n+ => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-}+ {-# SPECIALISE instance SingI n+ => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-}+ class (ListLike (f a) a) => LLF f a instance (ListLike (f a) a) => LLF f a @@ -80,14 +203,6 @@ instFunctor = weaken1 {-# INLINE instFunctor #-} -givenListLikeF :: ListLikeF f => ((Functor f, ListLike (f a) a) => f a -> b) -> f a -> b-givenListLikeF = withListLikeF Proxy-{-# INLINE givenListLikeF #-}--givenListLikeF' :: ListLikeF f => ((Functor f, ListLike (f a) a) => f a -> b) -> Sized f n a -> b-givenListLikeF' f = givenListLikeF f . runSized-{-# INLINE givenListLikeF' #-}- withListLikeF :: forall pxy f a b. ListLikeF f => pxy (f a) -> ((Functor f, ListLike (f a) a) => b) -> b withListLikeF _ b = b \\ llDic &&& instFunctor@@ -100,12 +215,4 @@ {-# INLINE withListLikeF' #-} toProxy :: a -> Proxy a-toProxy = const Proxy-{-# INLINE toProxy #-}--instance Class (FoldableLL f a) (ListLike f a) where- cls = Sub Dict--instance ListLike f a :=> FoldableLL f a where- ins = Sub Dict-+toProxy _ = Proxy
+ Data/Sized/Peano.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-}+{-# LANGUAGE ViewPatterns #-}+-- | This module exports @'S.Sized'@ type specialized to+-- type-level Peano numeral @'PN.Nat'@.+module Data.Sized.Peano+ (Ordinal, Sized, module Data.Sized,+ pattern (:<), pattern NilL, pattern (:>), pattern NilR) where+import Data.Sized hiding ((:<), (:>), NilL, NilR, Sized)+import qualified Data.Sized as S++import Data.ListLike (ListLike)+import Data.Singletons.Prelude (SingI)+import Data.Singletons.Prelude.Enum (PEnum (..))+import qualified Data.Type.Ordinal as O+import qualified Data.Type.Natural as PN++type Ordinal (n :: PN.Nat) = O.Ordinal n+type Sized f (n :: PN.Nat) = S.Sized f n++pattern (:<) :: forall f (n :: PN.Nat) a.+ (ListLike (f a) a)+ => forall (n1 :: PN.Nat).+ (n ~ Succ n1, SingI n1)+ => a -> Sized f n1 a -> Sized f n a+pattern a :< b = a S.:< b+infixr 5 :<++pattern NilL :: forall f (n :: PN.Nat) a.+ (ListLike (f a) a)+ => n ~ 'PN.Z => Sized f n a+pattern NilL = S.NilL++pattern (:>) :: forall f (n :: PN.Nat) a.+ (ListLike (f a) a)+ => forall (n1 :: PN.Nat).+ (n ~ Succ n1, SingI n1)+ => Sized f n1 a -> a -> Sized f n a+pattern a :> b = a S.:> b+infixl 5 :>++pattern NilR :: forall f (n :: PN.Nat) a.+ (ListLike (f a) a)+ => n ~ 'PN.Z => Sized f n a+pattern NilR = S.NilR
sized.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: sized-version: 0.1.0.0+version: 0.2.0.0 synopsis: Sized sequence data-types description: A wrapper to make length-parametrized data-type from ListLike data-types. license: BSD3@@ -20,14 +20,24 @@ library exposed-modules: Data.Sized+ , Data.Sized.Builtin+ , Data.Sized.Peano+ , Data.Sized.Flipped other-modules: Data.Sized.Internal -- other-extensions: - build-depends: base >=4.7 && <4.8- , type-natural- , ListLike- , vector- , containers- , constraints- , monomorphic+ build-depends: base >= 4.7 && <5+ , type-natural >= 0.4.1.1+ , mono-traversable >= 0.10 && < 1.1+ , ListLike+ , singletons >= 2.0+ , deepseq+ , hashable+ , vector+ , containers+ , constraints+ , equational-reasoning == 0.*+ , monomorphic+ , lens >= 0.14 -- hs-source-dirs: default-language: Haskell2010+ ghc-options: -Wall -Wno-redundant-constraints