diff --git a/sized.cabal b/sized.cabal --- a/sized.cabal +++ b/sized.cabal @@ -1,6 +1,6 @@ cabal-version: >=2.0 name: sized -version: 0.7.0.0 +version: 0.8.0.0 license: BSD3 license-file: LICENSE maintainer: konn.jinro_at_gmail.com diff --git a/src/Data/Sized.hs b/src/Data/Sized.hs --- a/src/Data/Sized.hs +++ b/src/Data/Sized.hs @@ -1,19 +1,14 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE UndecidableSuperClasses #-} -{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE AllowAmbiguousTypes, CPP, ConstraintKinds, DataKinds #-} {-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable, ExplicitNamespaces, FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving #-} -{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms #-} -{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction #-} -{-# LANGUAGE PatternSynonyms, PolyKinds, QuantifiedConstraints, ScopedTypeVariables, RankNTypes #-} -{-# LANGUAGE StandaloneDeriving, TypeApplications, TypeFamilies #-} -{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-} -#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 -{-# LANGUAGE NoStarIsType #-} -#endif +{-# LANGUAGE DeriveTraversable, DerivingStrategies, ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving, InstanceSigs, KindSignatures #-} +{-# LANGUAGE LambdaCase, LiberalTypeSynonyms, MultiParamTypeClasses #-} +{-# LANGUAGE NoMonomorphismRestriction, NoStarIsType, PatternSynonyms #-} +{-# LANGUAGE PolyKinds, QuantifiedConstraints, RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeApplications #-} +{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses, ViewPatterns #-} {-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-} {-# OPTIONS_GHC -fenable-rewrite-rules #-} @@ -35,13 +30,13 @@ length, sLength, null, -- ** Indexing (!!), (%!!), index, sIndex, head, last, - uncons, uncons', Uncons(..), + uncons, uncons', Uncons(..), unsnoc, unsnoc', Unsnoc(..), -- ** Slicing tail, init, take, takeAtMost, drop, splitAt, splitAtMost, -- * Construction -- ** Initialisation - empty, singleton, toSomeSized, replicate, replicate', generate, + empty, singleton, toSomeSized, replicate, replicate', generate, generate', -- ** Concatenation cons, (<|), snoc, (|>), append, (++), concat, -- ** Zips @@ -61,7 +56,7 @@ Partitioned(..), takeWhile, dropWhile, span, break, partition, -- ** Searching - elem, notElem, find, findIndex, sFindIndex, + elem, notElem, find, findIndex, sFindIndex, findIndices, sFindIndices, elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices, -- * Views and Patterns @@ -76,45 +71,54 @@ -- ** Definitions viewCons, ConsView (..), viewSnoc, SnocView(..), - pattern (:<), pattern NilL , pattern (:>), pattern NilR, + pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR, ) where import Data.Sized.Internal +import Control.Applicative (ZipList (..), (<*>)) +import Control.Subcategory (CApplicative (..), + CFoldable (..), CFreeMonoid (..), + CFunctor (..), CPointed (..), + CRepeat (..), CSemialign (..), + CTraversable (..), CUnzip (..), + CZip (..), Constrained (Dom), + cfromList, ctoList) +import Data.Coerce (coerce) +import Data.Constraint (Dict (..), withDict) import qualified Data.Foldable as F import Data.Kind (Type) -import Data.Monoid -import Control.Applicative ((<*>), ZipList(..)) import qualified Data.List as L +import Data.Maybe (fromJust) +import Data.Monoid (Monoid (..), (<>)) import qualified Data.Sequence as Seq -import Data.Singletons.Prelude.Bool -import Data.Constraint -import Data.Singletons.Prelude (SomeSing(..)) -import Data.Singletons.Prelude (SingI (..)) -import Data.Singletons.Prelude (withSing, withSingI) -import Control.Subcategory -import Data.Singletons.Prelude.Enum (sSucc, sPred, PEnum (..)) +import Data.Singletons.Prelude (SingI (..), SomeSing (..), + withSing, withSingI) +import Data.Singletons.Prelude.Bool (Sing) +import Data.Singletons.Prelude.Enum (PEnum (..), sPred, sSucc) +import Data.These (These (..)) +import Data.Type.Equality ((:~:) (..), gcastWith) import qualified Data.Type.Natural as Peano -import Data.Type.Natural.Class -import Data.Type.Ordinal (HasOrdinal, Ordinal (..)) -import Data.Type.Ordinal (ordToNatural) +import Data.Type.Natural.Class (type (-.), IsPeano (..), One, + PNum (..), POrd (..), + PeanoOrder (..), S, SNum (..), + Zero, pattern Zero, + ZeroOrSucc (..), sOne, sZero) +import Data.Type.Ordinal (HasOrdinal, Ordinal (..), + ordToNatural) 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 (fmap, uncurry, fromIntegral, const, Bool (..), Enum (..), Eq (..)) -import Prelude (Functor, Int, Maybe (..)) -import Prelude (Num (..), Ord (..), Ordering) -import Prelude (Show (..), flip, ($), (.)) +import Prelude (Bool (..), Enum (..), Eq (..), + Functor, Int, Maybe (..), + Num (..), Ord (..), Ordering, + Show (..), const, flip, fmap, + fromIntegral, uncurry, ($), (.)) import qualified Prelude as P +import Proof.Propositional (IsTrue (..), withWitness) import Unsafe.Coerce (unsafeCoerce) -import Data.Coerce (coerce) -import Data.Maybe (fromJust) -import Data.These (These(..)) -import Data.Type.Equality (gcastWith) -import Proof.Propositional (withWitness, IsTrue(Witness)) -import Data.Type.Equality ((:~:)(..)) -------------------------------------------------------------------------------- -- Main data-types @@ -153,10 +157,10 @@ -- If you use @unsafeFromList@ or similar unsafe functions, -- this function may return different value from type-parameterized length. -- --- Since 0.7.0.0 +-- Since 0.8.0.0 (type changed) length - :: forall nat f (n :: nat) a. - (IsPeano nat, CFoldable f, Dom f a, SingI n) + :: forall nat f (n :: nat) a. + (IsPeano nat, Dom f a, SingI n) => Sized f n a -> Int length = const $ fromIntegral $ toNatural $ sing @n {-# INLINE CONLIKE [1] length #-} @@ -176,12 +180,11 @@ -- | @Sing@ version of 'length'. -- --- Since 0.7.0.0 (type changed) -sLength :: forall nat f (n :: nat) a. (HasOrdinal nat, CFoldable f, Dom f a) +-- Since 0.8.0.0 (type changed) +sLength :: forall nat f (n :: nat) a. + (HasOrdinal nat, Dom f a, SingI n) => Sized f n a -> Sing n -sLength (Sized xs) = - case fromNatural (P.fromIntegral $ clength xs) of - SomeSing (n :: Sing (k :: nat)) -> unsafeCoerce n +sLength _ = sing @n {-# INLINE[2] sLength #-} -- | Test if the sequence is empty or not. @@ -211,12 +214,12 @@ {-# RULES "null/0" [~2] null = nullTL0 -"null/0" [~1] forall (vec :: (1 TL.<= n) => Sized f n a). - null vec = False "null/0" [~2] null = nullTLSucc +"null/0" [~1] forall (vec :: 1 TL.<= n => Sized f n a). + null vec = False "null/Z" [~2] null = nullPeano0 "null/Sn" [~2] null = nullPeanoSucc -#-} + #-} -------------------------------------------------------------------------------- --- Indexing @@ -236,7 +239,7 @@ -- -- Since 0.7.0.0 (%!!) - :: forall nat f (n :: nat) c. + :: forall nat f (n :: nat) c. (HasOrdinal nat, CFoldable f, Dom f c) => Sized f n c -> Ordinal n -> c (%!!) = coerce $ (. (P.fromIntegral . ordToNatural)) . cindex @f @c @@ -256,7 +259,7 @@ -- -- Since 0.7.0.0 index - :: forall nat f (m :: nat) a. + :: forall nat f (m :: nat) a. (CFoldable f, Dom f a, (One nat <= m) ~ 'True) => Int -> Sized f m a -> a index = flip (!!) @@ -277,7 +280,7 @@ -- -- Since 0.7.0.0 head - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (HasOrdinal nat, CFoldable f, Dom f a, (Zero nat < n) ~ 'True) => Sized f n a -> a head = coerce $ chead @f @a @@ -288,7 +291,7 @@ -- see <#ViewsAndPatterns Views and Patterns> section. -- -- Since 0.7.0.0 -last :: forall nat f (n :: nat) a. +last :: forall nat f (n :: nat) a. (HasOrdinal nat, (Zero nat < n) ~ 'True, CFoldable f, Dom f a) => Sized f n a -> a last = coerce $ clast @f @a @@ -299,17 +302,22 @@ -- see <#ViewsAndPatterns Views and Patterns> section. -- -- Since 0.7.0.0 -uncons :: forall nat f (n :: nat) a. +uncons :: forall nat f (n :: nat) a. (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True) => Sized f n a -> Uncons f n a uncons = withSingI (sPred $ sing @n) - $ gcastWith + $ gcastWith + (succAndPlusOneL $ sPred $ sing @n) + $ gcastWith (lneqRightPredSucc sZero (sing @n) Witness ) $ uncurry (Uncons @nat @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a) +-- | 'uncons' with explicit specified length @n@ +-- +-- Since 0.7.0.0 uncons' :: forall nat f (n :: nat) a proxy. (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) @@ -320,7 +328,7 @@ data Uncons f (n :: nat) a where Uncons :: forall nat f (n :: nat) a. SingI n - => a -> Sized f n a -> Uncons f (Succ n) a + => a -> Sized f n a -> Uncons f (One nat + n) a -- | Take the 'init' and 'last' of non-empty sequence. -- If you want to make case-analysis for general sequence, @@ -333,7 +341,7 @@ => Sized f n a -> Unsnoc f n a unsnoc = withSingI (sPred $ sing @n) - $ gcastWith + $ gcastWith (lneqRightPredSucc sZero (sing @n) Witness ) $ uncurry (Unsnoc @nat @f @(Pred n)) . coerce (fromJust . cunsnoc @f @a) @@ -342,11 +350,14 @@ data Unsnoc f n a where Unsnoc :: forall nat f n a. Sized f (n :: nat) a -> a -> Unsnoc f (Succ n) a +-- | 'unsnoc'' with explicit specified length @n@ +-- +-- Since 0.7.0.0 unsnoc' - :: forall nat f (n :: nat) a proxy. + :: forall nat f (n :: nat) a proxy. (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) => proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a -unsnoc' _ = +unsnoc' _ = withSingI (sSucc $ sing @n) $ withWitness (lneqZero $ sing @n) unsnoc {-# INLINE unsnoc' #-} @@ -389,7 +400,7 @@ take = coerce $ ctake @f @a . P.fromIntegral . toNatural @nat @n {-# INLINE take #-} --- | @take k xs@ takes first @k@ element of @xs@ at most. +-- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@. -- -- Since 0.7.0.0 takeAtMost @@ -489,7 +500,9 @@ replicate' = withSing replicate {-# INLINE replicate' #-} --- | Since 0.7.0.0 +-- | Construct a sequence of the given length by applying the function to each index. +-- +-- Since 0.7.0.0 generate :: forall (nat :: Type) f (n :: nat) (a :: Type). (CFreeMonoid f, Dom f a, HasOrdinal nat) @@ -499,6 +512,16 @@ . (. toEnum @(Ordinal n)) {-# INLINE [1] generate #-} +-- | 'generate' with length inferred. +-- +-- Since 0.8.0.0 +generate' + :: forall (nat :: Type) f (n :: nat) (a :: Type). + (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) + => (Ordinal n -> a) -> Sized f n a +generate' = generate sing +{-# INLINE [1] generate' #-} + genVector :: forall nat (n :: nat) a. (HasOrdinal nat) => Sing n -> (Ordinal n -> a) -> Sized V.Vector n a @@ -526,7 +549,7 @@ (f :: UV.Unbox a => Ordinal n -> a). generate n f = withSingI n $ Sized (UV.generate (P.fromIntegral $ toNatural n) (f . toEnum)) "generate/Seq" [~1] generate = genSeq -#-} + #-} -------------------------------------------------------------------------------- --- Concatenation @@ -534,20 +557,20 @@ -- | Append an element to the head of sequence. -- --- Since 0.7.0.0 +-- Since 0.8.0.0 cons - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) - => a -> Sized f n a -> Sized f (Succ n) a + => a -> Sized f n a -> Sized f (One nat + n) a cons = coerce $ ccons @f @a {-# INLINE cons #-} -- | Infix version of 'cons'. -- --- Since 0.7.0.0 +-- Since 0.8.0.0 (<|) :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) - => a -> Sized f n a -> Sized f (Succ n) a + => a -> Sized f n a -> Sized f (One nat + n) a (<|) = cons {-# INLINE (<|) #-} infixr 5 <| @@ -556,7 +579,7 @@ -- -- Since 0.7.0.0 snoc - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a snoc (Sized xs) a = Sized $ csnoc xs a @@ -565,7 +588,7 @@ -- | Infix version of 'snoc'. -- -- Since 0.7.0.0 -(|>) :: forall nat f (n :: nat) a. +(|>) :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a (|>) = snoc {-# INLINE (|>) #-} @@ -575,7 +598,7 @@ -- -- Since 0.7.0.0 append - :: forall nat f (n :: nat) (m :: nat) a. + :: forall nat f (n :: nat) (m :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> Sized f m a -> Sized f (n + m) a append = coerce $ mappend @(f a) @@ -585,7 +608,7 @@ -- -- Since 0.7.0.0 (++) - :: forall nat f (n :: nat) (m :: nat) a. + :: forall nat f (n :: nat) (m :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> Sized f m a -> Sized f (n + m) a (++) = append @@ -594,7 +617,7 @@ -- | Concatenates multiple sequences into one. -- -- Since 0.7.0.0 -concat :: forall nat f' (m :: nat) f (n :: nat) a. +concat :: forall nat f' (m :: nat) f (n :: nat) a. (CFreeMonoid f, CFunctor f', CFoldable f', Dom f a, Dom f' (f a), Dom f' (Sized f n a) ) @@ -619,7 +642,7 @@ -- -- Since 0.7.0.0 zipSame - :: forall nat f (n :: nat) a b. + :: forall nat f (n :: nat) a b. (Dom f a, CZip f, Dom f b, Dom f (a, b)) => Sized f n a -> Sized f n b -> Sized f n (a, b) zipSame = coerce $ czip @f @a @b @@ -629,7 +652,7 @@ -- -- Since 0.7.0.0 zipWith - :: forall nat f (n :: nat) a (m :: nat) b c. + :: forall nat f (n :: nat) a (m :: nat) b c. (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => (a -> b -> c) -> Sized f n a @@ -642,26 +665,9 @@ -- -- Since 0.7.0.0 zipWithSame - :: forall nat f (n :: nat) a b c. + :: forall nat f (n :: nat) a b c. (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c -{-# SPECIALISE INLINE [1] zipWithSame - :: (a -> b -> c) -> Sized [] n a -> Sized [] n b -> Sized [] n c - #-} -{-# SPECIALISE INLINE [1] zipWithSame - :: (a -> b -> c) - -> Sized V.Vector n a -> Sized V.Vector n b -> Sized V.Vector n c - #-} -{-# SPECIALISE INLINE [1] zipWithSame - :: (UV.Unbox a, UV.Unbox b, UV.Unbox c) - => (a -> b -> c) - -> Sized UV.Vector n a -> Sized UV.Vector n b -> Sized UV.Vector n c - #-} -{-# SPECIALISE INLINE [1] zipWithSame - :: (SV.Storable a, SV.Storable b, SV.Storable c) - => (a -> b -> c) - -> Sized SV.Vector n a -> Sized SV.Vector n b -> Sized SV.Vector n c - #-} zipWithSame = coerce $ czipWith @f @a @b @c {-# INLINE [1] zipWithSame #-} @@ -694,7 +700,7 @@ -- -- Since 0.7.0.0 map - :: forall nat f (n :: nat) a b. + :: forall nat f (n :: nat) a b. (CFreeMonoid f, Dom f a, Dom f b) => (a -> b) -> Sized f n a -> Sized f n b map f = Sized . cmap f . runSized @@ -732,7 +738,7 @@ -- | Sorting sequence by ascending order. -- -- Since 0.7.0.0 -sort :: forall nat f (n :: nat) a. +sort :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a, Ord a) => Sized f n a -> Sized f n a sort = coerce $ csort @f @a @@ -792,7 +798,7 @@ -- -- Since 0.7.0.0 (type changed) fromList - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => Sing n -> [a] -> Maybe (Sized f n a) fromList Zero _ = Just $ Sized (mempty :: f a) @@ -850,12 +856,12 @@ -- -- Since 0.5.0.0 (type changed) fromListWithDefault - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (HasOrdinal nat, Dom f a, CFreeMonoid f) => Sing n -> a -> [a] -> Sized f n a fromListWithDefault sn def xs = let len = P.fromIntegral $ toNatural sn - in Sized $ cfromList (ctake len xs) <> + in Sized $ cfromList (ctake len xs) <> creplicate (len - clength xs) def {-# INLINABLE fromListWithDefault #-} @@ -991,7 +997,11 @@ dropWhile = (toSomeSized .) . coerce (cdropWhile @f @a) {-# INLINE dropWhile #-} --- | Since 0.7.0.0 +-- | Split the sequence into the longest prefix +-- of elements that satisfy the predicate +-- and the rest. +-- +-- Since 0.7.0.0 span :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) @@ -999,7 +1009,11 @@ span = (unsafePartitioned @nat @n .) . coerce (cspan @f @a) {-# INLINE span #-} --- | Since 0.7.0.0 +-- | Split the sequence into the longest prefix +-- of elements that do not satisfy the +-- predicate and the rest. +-- +-- Since 0.7.0.0 break :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) @@ -1007,16 +1021,18 @@ break = (unsafePartitioned @nat @n .) . coerce (cbreak @f @a) {-# INLINE break #-} --- | Since 0.7.0.0 +-- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't. +-- +-- Since 0.7.0.0 partition - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => (a -> Bool) -> Sized f n a -> Partitioned f n a partition = (unsafePartitioned @nat @n .) . coerce (cpartition @f @a) {-# INLINE partition #-} unsafePartitioned - :: forall nat (n :: nat) f a. + :: forall nat (n :: nat) f a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => (f a, f a) -> Partitioned f n a unsafePartitioned (l, r) = @@ -1025,7 +1041,7 @@ SomeSized' (lenR :: Sing nr) rs ) -> gcastWith - (unsafeCoerce $ Refl @() + (unsafeCoerce $ Refl @() :: n :~: nl + nr ) $ Partitioned lenL ls lenR rs @@ -1037,7 +1053,7 @@ -- -- Since 0.7.0.0 elem - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> Bool elem = coerce $ celem @f @a @@ -1047,7 +1063,7 @@ -- -- Since 0.7.0.0 notElem - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> Bool notElem = coerce $ cnotElem @f @a @@ -1057,7 +1073,7 @@ -- -- Since 0.7.0.0 find - :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> Maybe a find = coerce $ cfind @f @a @@ -1077,7 +1093,7 @@ -- -- Since 0.7.0.0 findIndex - :: forall nat f (n :: nat) a . + :: forall nat f (n :: nat) a . (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> Maybe Int findIndex = coerce $ cfindIndex @f @a @@ -1087,13 +1103,12 @@ -- -- Since 0.7.0.0 sFindIndex - :: forall nat f (n :: nat) a . + :: forall nat f (n :: nat) a . (SingI (n :: nat), CFoldable f, Dom f a, HasOrdinal nat) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) sFindIndex = (fmap toEnum .) . coerce (cfindIndex @f @a) {-# INLINE sFindIndex #-} - -- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices. -- -- Since 0.7.0.0 @@ -1123,13 +1138,13 @@ -- | Returns the index of the given element in the list, if exists. -- -- Since 0.7.0.0 -elemIndex :: forall nat f (n :: nat) a . +elemIndex :: forall nat f (n :: nat) a . (CFoldable f, Eq a, Dom f a) => a -> Sized f n a -> Maybe Int elemIndex = coerce $ celemIndex @f @a {-# INLINE elemIndex #-} -- | Ordinal version of 'elemIndex'. --- Since 0.7.0.0, we no longer do boundary check inside the definition. +-- Since 0.7.0.0, we no longer do boundary check inside the definition. -- -- Since 0.7.0.0 sElemIndex, sUnsafeElemIndex :: forall nat f (n :: nat) a. @@ -1155,7 +1170,7 @@ -- -- Since 0.7.0.0 sElemIndices - :: forall nat f (n :: nat) a . + :: forall nat f (n :: nat) a . (CFoldable f, HasOrdinal nat, SingI (n :: nat), Dom f a, Eq a) => a -> Sized f n a -> [Ordinal n] sElemIndices = (fmap toEnum .) . elemIndices @@ -1205,14 +1220,14 @@ -- Since 0.7.0.0 data ConsView f n a where NilCV :: ConsView f (Zero nat) a - (:-) :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a + (:-) :: SingI n => a -> Sized f n a -> ConsView f (One nat + n) a infixr 5 :- -- | Case analysis for the cons-side of sequence. -- -- Since 0.5.0.0 (type changed) -viewCons :: forall nat f (n :: nat) a . +viewCons :: forall nat f (n :: nat) a . (HasOrdinal nat, SingI n, CFreeMonoid f,Dom f a) => Sized f n a -> ConsView f n a @@ -1220,9 +1235,9 @@ IsZero -> NilCV IsSucc n' -> withSingI n' - $ withSingI (sSucc n') + $ withSingI (sOne %+ n') $ case uncons' n' sz of - Uncons a xs -> (a :- xs) + Uncons a xs -> a :- xs -- | View of the left end of sequence (snoc-side). -- @@ -1235,14 +1250,14 @@ -- | Case analysis for the snoc-side of sequence. -- -- Since 0.5.0.0 (type changed) -viewSnoc :: forall nat f (n :: nat) a. +viewSnoc :: forall nat f (n :: nat) a. (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) => Sized f n a -> SnocView f n a viewSnoc sz = case zeroOrSucc (sing @n) of IsZero -> NilSV IsSucc (n' :: Sing n') -> - withSingI n' $ + withSingI n' $ gcastWith (succAndPlusOneR n') $ case unsnoc' n' sz of Unsnoc (xs :: Sized f m a) a -> @@ -1271,14 +1286,13 @@ @ slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n -slen 'NilL' = 'SZ' +slen 'Nil' = 'SZ' slen (_ ':<' as) = 'SS' (slen as) -slen _ = error "impossible" @ - So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to + So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) 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, + @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors, but pattern synonyms so we cannot use them in expression contexts. For more detail on pattern synonyms, see @@ -1289,40 +1303,62 @@ infixr 5 :< -- | Pattern synonym for cons-side uncons. pattern (:<) - :: forall nat (f :: Type -> Type) a (n :: nat). + :: forall nat (f :: Type -> Type) a (n :: nat). (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f) - => forall (n1 :: nat). (n ~ Succ n1, SingI n1) + => forall (n1 :: nat). (n ~ (One nat + n1), SingI n1) => a -> Sized f n1 a -> Sized f n a pattern a :< as <- (viewCons -> a :- as) where a :< as = a <| as +chkNil + :: forall nat f (n :: nat) a. + (IsPeano nat, SingI n) + => Sized f n a -> ZeroOrSucc n +chkNil = const $ zeroOrSucc $ sing @n + +-- | Pattern synonym for a nil sequence. +pattern Nil :: forall nat f (n :: nat) a. + (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) + => (n ~ Zero nat) => Sized f n a +pattern Nil <- (chkNil -> IsZero) where + Nil = empty + +-- | Pattern synonym for cons-side nil. +{-# DEPRECATED NilL "Use Nil instead" #-} pattern NilL :: forall nat f (n :: nat) a. (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) => (n ~ Zero nat) => Sized f n a -pattern NilL <- (viewCons -> NilCV) where - NilL = empty +pattern NilL = Nil infixl 5 :> +-- | Pattern synonym for snoc-side unsnoc. pattern (:>) - :: forall nat (f :: Type -> Type) a (n :: nat). + :: forall nat (f :: Type -> Type) a (n :: nat). (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f) => forall (n1 :: nat). (n ~ (n1 + One nat), SingI n1) => Sized f n1 a -> a -> Sized f n a pattern a :> b <- (viewSnoc -> a :-:: b) where a :> b = a |> b +{-# DEPRECATED NilR "Use Nil instead" #-} pattern NilR :: forall nat f (n :: nat) a. (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) => n ~ Zero nat => Sized f n a -pattern NilR <- (viewSnoc -> NilSV) where - NilR = empty +pattern NilR = Nil +{-# COMPLETE (:<), Nil #-} +{-# COMPLETE (:<), NilL #-} +{-# COMPLETE (:<), NilR #-} +{-# COMPLETE (:>), Nil #-} +{-# COMPLETE (:>), NilL #-} +{-# COMPLETE (:>), NilR #-} + class Dom f a => DomC f a instance Dom f a => DomC f a -- | Applicative instance, generalizing @'Data.Monoid.ZipList'@. -instance +instance ( Functor f, CFreeMonoid f, CZip f, HasOrdinal nat, SingI n, forall a. DomC f a) => P.Applicative (Sized f (n :: nat)) where @@ -1364,7 +1400,7 @@ -- we require more strong 'CZip' constraint here. instance (CZip f, CFreeMonoid f) => CSemialign (Sized f n) where calignWith = coerce (\f -> czipWith @f @a @b @c ((f .) . These)) - :: forall a b c. + :: forall a b c. (Dom f a, Dom f b, Dom f c) => (These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c {-# INLINE [1] calignWith #-} @@ -1372,11 +1408,11 @@ :: forall a b. (Dom f a, Dom f b, Dom f (These a b)) => Sized f n a -> Sized f n b -> Sized f n (These a b) - {-# INLINE [1] calign #-} + {-# INLINE [1] calign #-} instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where czipWith = coerce $ czipWith @f @a @b @c - :: forall a b c. + :: forall a b c. (Dom f a, Dom f b, Dom f c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c {-# INLINE [1] czipWith #-} @@ -1384,13 +1420,13 @@ :: forall a b. (Dom f a, Dom f b, Dom f (a, b)) => Sized f n a -> Sized f n b -> Sized f n (a, b) - {-# INLINE [1] czip #-} + {-# INLINE [1] czip #-} -instance +instance (PeanoOrder nat, SingI (n :: nat), CZip f, CFreeMonoid f) => CRepeat (Sized f n) where crepeat = replicate' - {-# INLINE [1] crepeat #-} + {-# INLINE [1] crepeat #-} instance CTraversable f => CTraversable (Sized f n) where ctraverse = \f -> fmap coerce . ctraverse f . runSized diff --git a/src/Data/Sized/Builtin.hs b/src/Data/Sized/Builtin.hs --- a/src/Data/Sized/Builtin.hs +++ b/src/Data/Sized/Builtin.hs @@ -4,12 +4,20 @@ {-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE KindSignatures #-} {-# LANGUAGE NoStarIsType #-} --- | This module exports @'S.Sized'@ type and --- functions specialized to --- GHC's built-in type numeral @'Nat'@. +-- | This module exports provides the functionality to make length-parametrized types +-- from existing 'CFreeMonoid' sequential types, +-- parametrised with GHC's built in 'Nat' kind. +-- +-- Most of the complexity of operations on @'Sized' f n a@ are the same as +-- original operations on @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 <#ViewsAndPatterns Views and Patterns> for more detail. module Data.Sized.Builtin - ( -- * Main Data-types + ( -- * Main Data-types Sized(), SomeSized, pattern SomeSized, Ordinal, DomC(), -- * Accessors @@ -23,7 +31,7 @@ tail, init, take, takeAtMost, drop, splitAt, splitAtMost, -- * Construction -- ** Initialisation - empty, singleton, toSomeSized, replicate, replicate', generate, + empty, singleton, toSomeSized, replicate, replicate', generate, generate', -- ** Concatenation cons, (<|), snoc, (|>), append, (++), concat, -- ** Zips @@ -57,11 +65,11 @@ -- ** Definitions viewCons, ConsView, - pattern (S.:-), pattern S.NilCV, + pattern (:-), pattern NilCV, viewSnoc, SnocView, - pattern (S.:-::), pattern S.NilSV, + pattern (:-::), pattern NilSV, - pattern (:<), pattern NilL , pattern (:>), pattern NilR, + pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR, ) where import qualified Data.Sized as S import Data.Sized (DomC) @@ -79,8 +87,22 @@ import Data.Type.Natural (Min, type (-), type (+), type (*)) type Ordinal = (O.Ordinal :: Nat -> Type) + +-- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version. +-- +-- Here, 'f' must satisfy @'CFreeMonoid' f@ and @Dom f a@. +-- +-- Since 0.2.0.0 type Sized = (S.Sized :: (Type -> Type) -> Nat -> Type -> Type) +-- | 'Sized' sequence 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.7.0.0 type SomeSized f a = S.SomeSized' f Nat a pattern SomeSized @@ -90,58 +112,125 @@ {-# COMPLETE SomeSized #-} pattern SomeSized n s = S.SomeSized' n s -length :: (Dom f a, CFoldable f, KnownNat n) => 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.8.0.0 (type changed) +{-# INLINE length #-} +length :: (Dom f a, KnownNat n) => Sized f n a -> Int length = S.length @Nat -sLength :: (Dom f a, CFoldable f) => Sized f n a -> SNat n +-- | @Sing@ version of 'length'. +-- +-- Since 0.8.0.0 (type changed) +sLength :: (Dom f a, KnownNat n) => Sized f n a -> SNat n +{-# INLINE sLength #-} sLength = S.sLength @Nat +-- | Test if the sequence is empty or not. +-- +-- Since 0.7.0.0 null :: (Dom f a, CFoldable f) => Sized f n a -> Bool +{-# INLINE null #-} null = S.null @Nat +-------------------------------------------------------------------------------- +--- Indexing +-------------------------------------------------------------------------------- + +-- | (Unsafe) indexing with @Int@s. +-- If you want to check boundary statically, use '%!!' or 'sIndex'. +-- +-- Since 0.7.0.0 (!!) :: (Dom f a, CFoldable f, (1 <= m) ~ 'True) => Sized f m a -> Int -> a +{-# INLINE (!!) #-} (!!) = (S.!!) @Nat +-- | Safe indexing with 'Ordinal's. +-- +-- Since 0.7.0.0 (%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c +{-# INLINE (%!!) #-} (%!!) = (S.%!!) @Nat +-- | Flipped version of '!!'. +-- +-- Since 0.7.0.0 index :: (Dom f a, CFoldable f, (1 <= m) ~ 'True) => Int -> Sized f m a -> a +{-# INLINE index #-} index = S.index @Nat +-- | Flipped version of '%!!'. +-- +-- Since 0.7.0.0 sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c +{-# INLINE sIndex #-} sIndex = S.sIndex @Nat +-- | 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.7.0.0 head :: (Dom f a, CFoldable f, (0 < n) ~ 'True) => Sized f n a -> a +{-# INLINE head #-} head = S.head @Nat +-- | 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.7.0.0 last :: (Dom f a, CFoldable f, (0 < n) ~ 'True) => Sized f n a -> a +{-# INLINE last #-} last = S.last @Nat +-- | 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.7.0.0 uncons :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) => Sized f n a -> Uncons f n a +{-# INLINE uncons #-} uncons = S.uncons @Nat +-- | 'uncons' with explicit specified length @n@ +-- +-- Since 0.7.0.0 uncons' :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) => Sized f n a -> Uncons f n a +{-# INLINE uncons' #-} uncons' = S.uncons @Nat +-- | 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.7.0.0 unsnoc :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) => Sized f n a -> Unsnoc f n a +{-# INLINE unsnoc #-} unsnoc = S.unsnoc @Nat +-- | 'unsnoc'' with explicit specified length @n@ +-- +-- Since 0.7.0.0 unsnoc' :: (Dom f a, KnownNat n, CFreeMonoid f) => proxy n -> Sized f (n + 1) a -> Unsnoc f (n + 1) a +{-# INLINE unsnoc' #-} unsnoc' = S.unsnoc' @Nat type Uncons f (n :: Nat) a = S.Uncons f n a pattern Uncons :: forall (f :: Type -> Type) (n :: Nat) a. () - => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) + => forall (n1 :: Nat). (n ~ (1 + n1), SingI n1) => a -> Sized f n1 a -> Uncons f n a pattern Uncons a as = S.Uncons a as @@ -153,186 +242,453 @@ => Sized f n1 a -> a -> Unsnoc f n a pattern Unsnoc xs x = S.Unsnoc xs x +-- | 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.7.0.0 tail :: (Dom f a, CFreeMonoid f) => Sized f (1 + n) a -> Sized f n a +{-# INLINE tail #-} tail = S.tail @Nat +-- | 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.7.0.0 init :: (Dom f a, CFreeMonoid f) => Sized f (n + 1) a -> Sized f n a +{-# INLINE init #-} init = S.init @Nat +-- | @take k xs@ takes first @k@ element of @xs@ where +-- the length of @xs@ should be larger than @k@. +-- +-- Since 0.7.0.0 take :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> Sized f n a +{-# INLINE take #-} take = S.take @Nat +-- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@. +-- +-- Since 0.7.0.0 takeAtMost :: (Dom f a, CFreeMonoid f) => SNat n -> Sized f m a -> Sized f (Min n m) a +{-# INLINE takeAtMost #-} takeAtMost = S.takeAtMost @Nat +-- | @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@. +-- +-- Since 0.7.0.0 drop :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> Sized f (m - n) a +{-# INLINE drop #-} drop = S.drop @Nat +-- | @splitAt k xs@ split @xs@ at @k@, where +-- the length of @xs@ should be less than or equal to @k@. +-- +-- Since 0.7.0.0 splitAt :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a) +{-# INLINE splitAt #-} splitAt = S.splitAt @Nat +-- | @splitAtMost k xs@ split @xs@ at @k@. +-- If @k@ exceeds the length of @xs@, then the second result value become empty. +-- +-- Since 0.7.0.0 splitAtMost :: (Dom f a, CFreeMonoid f) => SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a) +{-# INLINE splitAtMost #-} splitAtMost = S.splitAtMost @Nat +-------------------------------------------------------------------------------- +-- Construction +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Initialisation +-------------------------------------------------------------------------------- + +-- | Empty sequence. +-- +-- Since 0.7.0.0 (type changed) empty :: (Dom f a, Monoid (f a)) => Sized f 0 a +{-# INLINE empty #-} empty = S.empty @Nat +-- | Sequence with one element. +-- +-- Since 0.7.0.0 singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f 1 a +{-# INLINE singleton #-} singleton = S.singleton @Nat + +-- | Consruct the 'Sized' sequence from base type, but +-- the length parameter is dynamically determined and +-- existentially quantified; see also 'SomeSized''. +-- +-- Since 0.7.0.0 toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a +{-# INLINE toSomeSized #-} toSomeSized = S.toSomeSized @Nat +-- | Replicates the same value. +-- +-- Since 0.7.0.0 replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a +{-# INLINE replicate #-} replicate = S.replicate @Nat +-- | 'replicate' with the length inferred. +-- +-- Since 0.7.0.0 replicate' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> Sized f n a +{-# INLINE replicate' #-} replicate' = S.replicate' @Nat +-- | Construct a sequence of the given length by applying the function to each index. +-- +-- Since 0.7.0.0 generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a +{-# INLINE generate #-} generate = S.generate @Nat -cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (n + 1) a +-- | 'generate' with length inferred. +-- +-- Since 0.8.0.0 +generate' + :: forall f n a. (KnownNat n, Dom f a, CFreeMonoid f) => (Ordinal n -> a) -> Sized f n a +{-# INLINE generate' #-} +generate' = S.generate' @Nat + +-------------------------------------------------------------------------------- +--- Concatenation +-------------------------------------------------------------------------------- + +-- | Append an element to the head of sequence. +-- +-- Since 0.7.0.0 +cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (1 + n) a +{-# INLINE cons #-} cons = S.cons @Nat +-- | Append an element to the tail of sequence. +-- +-- Since 0.7.0.0 snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a +{-# INLINE snoc #-} snoc = S.snoc @Nat -(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (n + 1) a +-- | Infix version of 'snoc'. +-- +-- Since 0.7.0.0 +(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (1 + n) a +{-# INLINE (<|) #-} (<|) = (S.<|) @Nat +-- | Append an element to the tail of sequence. +-- +-- Since 0.7.0.0 (|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a +{-# INLINE (|>) #-} (|>) = (S.|>) @Nat +-- | Infix version of 'append'. +-- +-- Since 0.7.0.0 (++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a +{-# INLINE (++) #-} (++) = (S.++) @Nat +-- | Append two lists. +-- +-- Since 0.7.0.0 append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a +{-# INLINE append #-} append = S.append @Nat +-- | Concatenates multiple sequences into one. +-- +-- Since 0.7.0.0 concat :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a), CFreeMonoid f, CFunctor f', CFoldable f' ) => Sized f' m (Sized f n a) -> Sized f (m * n) a +{-# INLINE concat #-} concat = S.concat @Nat + +-------------------------------------------------------------------------------- +--- Zips +-------------------------------------------------------------------------------- + +-- | Zipping two sequences. Length is adjusted to shorter one. +-- +-- Since 0.7.0.0 zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f) => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) +{-# INLINE zip #-} zip = S.zip @Nat +-- | 'zip' for the sequences of the same length. +-- +-- Since 0.7.0.0 zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f) => Sized f n a -> Sized f n b -> Sized f n (a, b) +{-# INLINE zipSame #-} zipSame = S.zipSame @Nat +-- | Zipping two sequences with funtion. Length is adjusted to shorter one. +-- +-- Since 0.7.0.0 zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c +{-# INLINE zipWith #-} zipWith = S.zipWith @Nat +-- | 'zipWith' for the sequences of the same length. +-- +-- Since 0.7.0.0 zipWithSame :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c +{-# INLINE zipWithSame #-} zipWithSame = S.zipWithSame @Nat +-- | Unzipping the sequence of tuples. +-- +-- Since 0.7.0.0 unzip :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f) => Sized f n (a, b) -> (Sized f n a, Sized f n b) +{-# INLINE unzip #-} unzip = S.unzip @Nat +-- | Unzipping the sequence of tuples. +-- +-- Since 0.7.0.0 unzipWith :: (Dom f a, Dom f b, Dom f c, CUnzip f) => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c) +{-# INLINE unzipWith #-} unzipWith = S.unzipWith @Nat +-------------------------------------------------------------------------------- +-- Transformation +-------------------------------------------------------------------------------- + +-- | Map function. +-- +-- Since 0.7.0.0 map :: (Dom f a, Dom f b, CFreeMonoid f) => (a -> b) -> Sized f n a -> Sized f n b +{-# INLINE map #-} map = S.map @Nat +-- | Reverse function. +-- +-- Since 0.7.0.0 reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a +{-# INLINE reverse #-} reverse = S.reverse @Nat +-- | Intersperces. +-- +-- Since 0.7.0.0 intersperse :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ((2 * n) -. 1) a +{-# INLINE intersperse #-} intersperse = S.intersperse @Nat +-- | Remove all duplicates. +-- +-- Since 0.7.0.0 nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a +{-# INLINE nub #-} nub = S.nub @Nat +-- | Sorting sequence by ascending order. +-- +-- Since 0.7.0.0 sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a +{-# INLINE sort #-} sort = S.sort @Nat +-- | Generalized version of 'sort'. +-- +-- Since 0.7.0.0 sortBy :: (Dom f a, CFreeMonoid f) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a +{-# INLINE sortBy #-} sortBy = S.sortBy @Nat +-- | Insert new element into the presorted sequence. +-- +-- Since 0.7.0.0 insert :: (Dom f a, CFreeMonoid f, Ord a) => a -> Sized f n a -> Sized f (n + 1) a +{-# INLINE insert #-} insert = S.insert @Nat +-- | Generalized version of 'insert'. +-- +-- Since 0.7.0.0 +{-# INLINE insertBy #-} insertBy :: (Dom f a, CFreeMonoid f) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (n + 1) a insertBy = S.insertBy @Nat +-------------------------------------------------------------------------------- +-- Conversion +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- List +-------------------------------------------------------------------------------- + +-- | Convert to list. +-- +-- Since 0.7.0.0 +{-# INLINE toList #-} toList :: (Dom f a, CFoldable f) => Sized f n a -> [a] toList = S.toList @Nat +-- | 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.7.0.0 (type changed) +{-# INLINE fromList #-} fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a) fromList = S.fromList @Nat +-- | 'fromList' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE fromList' #-} fromList' :: (Dom f a, CFreeMonoid f, KnownNat n) => [a] -> Maybe (Sized f n a) fromList' = S.fromList' @Nat +-- | Unsafe version of 'fromList'. If the length of the given list does not +-- equal to @n@, then something unusual happens. +-- +-- Since 0.7.0.0 +{-# INLINE unsafeFromList #-} unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a unsafeFromList = S.unsafeFromList @Nat +-- | 'unsafeFromList' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE unsafeFromList' #-} unsafeFromList' :: (Dom f a, KnownNat n, CFreeMonoid f) => [a] -> Sized f n a unsafeFromList' = S.unsafeFromList' @Nat +-- | Construct a @Sized f n a@ by padding default value if the given list is short. +-- +-- Since 0.5.0.0 (type changed) +{-# INLINE fromListWithDefault #-} fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a fromListWithDefault = S.fromListWithDefault @Nat +-- | 'fromListWithDefault' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE fromListWithDefault' #-} fromListWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> [a] -> Sized f n a fromListWithDefault' = S.fromListWithDefault' @Nat +-------------------------------------------------------------------------------- +--- Base containes +-------------------------------------------------------------------------------- + +-- | Forget the length and obtain the wrapped base container. +-- +-- Since 0.7.0.0 +{-# INLINE unsized #-} unsized :: Sized f n a -> f a unsized = S.unsized @Nat +-- | 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.7.0.0 +{-# INLINE toSized #-} toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a) toSized = S.toSized @Nat +-- | 'toSized' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE toSized' #-} toSized' :: (Dom f a, CFreeMonoid f, KnownNat n) => f a -> Maybe (Sized f n a) toSized' = S.toSized' @Nat +-- | Unsafe version of 'toSized'. If the length of the given list does not +-- equal to @n@, then something unusual happens. +-- +-- Since 0.7.0.0 +{-# INLINE unsafeToSized #-} unsafeToSized :: SNat n -> f a -> Sized f n a unsafeToSized = S.unsafeToSized @Nat +-- | 'unsafeToSized' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE unsafeToSized' #-} unsafeToSized' :: (Dom f a, KnownNat n) => f a -> Sized f n a unsafeToSized' = S.unsafeToSized' @Nat +-- | Construct a @Sized f n a@ by padding default value if the given list is short. +-- +-- Since 0.7.0.0 +{-# INLINE toSizedWithDefault #-} toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a toSizedWithDefault = S.toSizedWithDefault @Nat +-- | 'toSizedWithDefault' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE toSizedWithDefault' #-} toSizedWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> f a -> Sized f n a toSizedWithDefault' = S.toSizedWithDefault' @Nat +-------------------------------------------------------------------------------- +-- Querying +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Partitioning +-------------------------------------------------------------------------------- + +-- | 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.7.0.0 type Partitioned f (n :: Nat) a = S.Partitioned f n a pattern Partitioned @@ -343,90 +699,310 @@ {-# COMPLETE Partitioned #-} pattern Partitioned ls l rs r = S.Partitioned ls l rs r +-- | Take the initial segment as long as elements satisfys the predicate. +-- +-- Since 0.7.0.0 +{-# INLINE takeWhile #-} takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a takeWhile = S.takeWhile @Nat +-- | Drop the initial segment as long as elements satisfys the predicate. +-- +-- Since 0.7.0.0 +{-# INLINE dropWhile #-} dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a dropWhile = S.dropWhile @Nat +-- | Split the sequence into the longest prefix +-- of elements that satisfy the predicate +-- and the rest. +-- +-- Since 0.7.0.0 span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a +{-# INLINE span #-} span = S.span @Nat +-- | Split the sequence into the longest prefix +-- of elements that do not satisfy the +-- predicate and the rest. +-- +-- Since 0.7.0.0 +{-# INLINE break #-} break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a break = S.break @Nat +-- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't. +-- +-- Since 0.7.0.0 +{-# INLINE partition #-} partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a partition = S.partition @Nat +-------------------------------------------------------------------------------- +--- Searching +-------------------------------------------------------------------------------- +-- | Membership test; see also 'notElem'. +-- +-- Since 0.7.0.0 +{-# INLINE elem #-} elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool elem = S.elem @Nat +-- | Negation of 'elem'. +-- +-- Since 0.7.0.0 +{-# INLINE notElem #-} notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool notElem = S.notElem @Nat +-- | Find the element satisfying the predicate. +-- +-- Since 0.7.0.0 +{-# INLINE find #-} find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a find = S.find @Nat +-- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists. +-- +-- Since 0.7.0.0 +{-# INLINE findIndex #-} findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int findIndex = S.findIndex @Nat +-- | 'Ordinal' version of 'findIndex'. +-- +-- Since 0.7.0.0 +{-# INLINE sFindIndex #-} sFindIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) sFindIndex = S.sFindIndex @Nat +-- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices. +-- +-- Since 0.7.0.0 +{-# INLINE findIndices #-} findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int] findIndices = S.findIndices @Nat +-- | 'Ordinal' version of 'findIndices'. +-- +-- Since 0.7.0.0 +{-# INLINE sFindIndices #-} sFindIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n] sFindIndices = S.sFindIndices @Nat -elemIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int -elemIndex = S.findIndex @Nat +-- | Returns the index of the given element in the list, if exists. +-- +-- Since 0.8.0.0 +{-# INLINE elemIndex #-} +elemIndex :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Maybe Int +elemIndex = S.elemIndex @Nat -sUnsafeElemIndex :: (Dom f a, KnownNat n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n) +sElemIndex, sUnsafeElemIndex :: (Dom f a, KnownNat n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n) {-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-} + +-- | Ordinal version of 'elemIndex'. +-- Since 0.7.0.0, we no longer do boundary check inside the definition. +-- +-- Since 0.7.0.0 sUnsafeElemIndex = S.sElemIndex @Nat -sElemIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) -sElemIndex = S.sFindIndex @Nat +-- | Ordinal version of 'elemIndex'. +-- Since 0.7.0.0, we no longer do boundary check inside the definition. +-- +-- Since 0.7.0.0 +sElemIndex = S.sElemIndex @Nat -elemIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int] -elemIndices = S.findIndices @Nat +-- | Returns all indices of the given element in the list. +-- +-- Since 0.8.0.0 +{-# INLINE elemIndices #-} +elemIndices :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> [Int] +elemIndices = S.elemIndices @Nat -sElemIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n] -sElemIndices = S.sFindIndices @Nat +-- | Ordinal version of 'elemIndices' +-- +-- Since 0.8.0.0 +{-# INLINE sElemIndices #-} +sElemIndices + :: (Dom f a, CFoldable f, KnownNat n, Eq a) + => a -> Sized f n a -> [Ordinal n] +sElemIndices = S.sElemIndices @Nat -type ConsView f (n :: Nat) a = S.ConsView f n a +-------------------------------------------------------------------------------- +-- Views and Patterns +-------------------------------------------------------------------------------- +{-$ViewsAndPatterns #ViewsAndPatterns# + + With GHC's @ViewPatterns@ and @PatternSynonym@ extensions, + we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor. + Curretnly, there are two direction view and patterns: Cons and Snoc. + Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead' + (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on + cons (resp. snoc) of @Sized f n a@ in O(1). +-} + +{-$views #views# + + With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows: + +@ +slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n +slen ('viewCons' -> 'NilCV') = 'SZ' +slen ('viewCons' -> _ ':-' as) = 'SS' (slen as) +slen _ = error "impossible" +@ + + The constraint @('KnownNat' n, 'Dom f 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 :: ('KnownNat' n, 'Dom f 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.7.0.0 +type ConsView = + (S.ConsView :: (Type -> Type) -> Nat -> Type -> Type) + +-- | Since 0.8.0.0 +pattern NilCV + :: forall (f :: Type -> Type) n a. () + => (n ~ 0) + => ConsView f n a +pattern NilCV = S.NilCV + +-- | Since 0.8.0.0 +pattern (:-) + :: forall (f :: Type -> Type) n a. () + => forall n1. (n ~ (1 + n1), SingI n1) + => a -> Sized f n1 a -> ConsView f n a +pattern l :- ls = l S.:- ls + +infixr 9 :- +{-# COMPLETE NilCV, (:-) #-} + +-- | Case analysis for the cons-side of sequence. +-- +-- Since 0.5.0.0 (type changed) viewCons :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a viewCons = S.viewCons @Nat -type SnocView f (n :: Nat) a = S.SnocView f n a +-- | View of the left end of sequence (snoc-side). +-- +-- Since 0.7.0.0 +type SnocView = + (S.SnocView :: (Type -> Type) -> Nat -> Type -> Type) -viewSnoc :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a -viewSnoc = S.viewCons @Nat +-- | Since 0.8.0.0 +pattern NilSV + :: forall (f :: Type -> Type) n a. () + => (n ~ 0) + => SnocView f n a +pattern NilSV = S.NilSV + +infixl 9 :-:: +-- | Since 0.8.0.0 +pattern (:-::) + :: forall (f :: Type -> Type) n a. () + => forall n1. (n ~ (n1 + 1), SingI n1) + => Sized f n1 a -> a -> SnocView f n a +pattern ls :-:: l = ls S.:-:: l +{-# COMPLETE NilSV, (:-::) #-} + + +-- | Case analysis for the snoc-side of sequence. +-- +-- Since 0.8.0.0 (type changed) +viewSnoc :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> SnocView f n a +viewSnoc = S.viewSnoc @Nat + +{-$patterns #patterns# + + So we can pattern match on both end of sequence via views, but + it is rather clumsy to nest it. For example: + +@ +nextToHead :: ('Dom f 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 :: ('Dom f 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, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n +slen 'Nil' = 'SZ' +slen (_ ':<' as) = 'SS' (slen as) +@ + + So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to + pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. + @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors, + but pattern synonyms so we cannot use them in expression contexts. + For more detail on pattern synonyms, see + + and + . +-} + +-- | Pattern synonym for cons-side uncons. pattern (:<) :: forall (f :: Type -> Type) a (n :: Nat). - (Dom f a, SingI n, CFreeMonoid f) - => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) + (Dom f a, KnownNat n, CFreeMonoid f) + => forall (n1 :: Nat). (n ~ (1 + n1), SingI n1) => a -> Sized f n1 a -> Sized f n a pattern a :< b = a S.:< b infixr 5 :< +-- | Pattern synonym for a nil sequence. +pattern Nil + :: forall (f :: Type -> Type) a n. + (Dom f a, KnownNat n, CFreeMonoid f) + => (n ~ 0) => Sized f n a +pattern Nil = S.Nil + +{-# DEPRECATED NilL "Use Nil instead" #-} +-- | Pattern synonym for cons-side nil. pattern NilL :: forall f (n :: Nat) a. (KnownNat n, CFreeMonoid f, Dom f a) => n ~ 0 => Sized f n a -pattern NilL = S.NilL +pattern NilL = Nil +-- | Pattern synonym for snoc-side unsnoc. pattern (:>) :: forall (f :: Type -> Type) a (n :: Nat). - (Dom f a, SingI n, CFreeMonoid f) + (Dom f a, KnownNat n, CFreeMonoid f) => forall (n1 :: Nat). (n ~ (n1 + 1), SingI n1) => Sized f n1 a -> a -> Sized f n a pattern a :> b = a S.:> b infixl 5 :> +{-# DEPRECATED NilR "Use Nil instead" #-} +-- | Pattern synonym for snoc-side nil. pattern NilR :: forall f (n :: Nat) a. - (CFreeMonoid f, Dom f a, SingI n) + (CFreeMonoid f, Dom f a, KnownNat n) => n ~ 0 => Sized f n a -pattern NilR = S.NilR +pattern NilR = Nil +{-# COMPLETE (:<), NilL #-} +{-# COMPLETE (:<), NilR #-} +{-# COMPLETE (:<), Nil #-} +{-# COMPLETE (:>), NilL #-} +{-# COMPLETE (:>), NilR #-} +{-# COMPLETE (:>), Nil #-} diff --git a/src/Data/Sized/Peano.hs b/src/Data/Sized/Peano.hs --- a/src/Data/Sized/Peano.hs +++ b/src/Data/Sized/Peano.hs @@ -5,10 +5,18 @@ {-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE NoStarIsType #-} --- | This module exports @'S.Sized'@ type specialized to --- type-level Peano numeral @'PN.Nat'@. +-- | This module exports provides the functionality to make length-parametrized types +-- from existing 'CFreeMonoid' sequential types, +-- parametrised with peano numeral 'PN.Nat' kind. +-- +-- Most of the complexity of operations on @'Sized' f n a@ are the same as +-- original operations on @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 <#ViewsAndPatterns Views and Patterns> for more detail. module Data.Sized.Peano - ( -- * Main Data-types + ( -- * Main Data-types Sized(), SomeSized, pattern SomeSized, Ordinal, DomC(), -- * Accessors @@ -22,7 +30,7 @@ tail, init, take, takeAtMost, drop, splitAt, splitAtMost, -- * Construction -- ** Initialisation - empty, singleton, toSomeSized, replicate, replicate', generate, + empty, singleton, toSomeSized, replicate, replicate', generate, generate', -- ** Concatenation cons, (<|), snoc, (|>), append, (++), concat, -- ** Zips @@ -56,11 +64,11 @@ -- ** Definitions viewCons, ConsView, - pattern (S.:-), pattern S.NilCV, + pattern (:-), pattern NilCV, viewSnoc, SnocView, - pattern (S.:-::), pattern S.NilSV, + pattern (:-::), pattern NilSV, - pattern (:<), pattern NilL , pattern (:>), pattern NilR, + pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR, ) where import qualified Data.Sized as S import Data.Sized (DomC) @@ -78,8 +86,23 @@ import Data.Type.Natural (One) type Ordinal = (O.Ordinal :: Nat -> Type) + +-- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version. +-- +-- Here, 'f' must satisfy @'CFreeMonoid' f@ and @Dom f a@. +-- +-- Since 0.2.0.0 type Sized = (S.Sized :: (Type -> Type) -> Nat -> Type -> Type) + +-- | 'Sized' sequence 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.7.0.0 type SomeSized f a = S.SomeSized' f Nat a pattern SomeSized @@ -89,51 +112,118 @@ {-# COMPLETE SomeSized #-} pattern SomeSized n s = S.SomeSized' n s -length :: (Dom f a, CFoldable f, SingI n) => 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.8.0.0 (type changed) +{-# INLINE length #-} +length :: (Dom f a, SingI n) => Sized f n a -> Int length = S.length @Nat -sLength :: (Dom f a, CFoldable f) => Sized f n a -> SNat n +-- | @Sing@ version of 'length'. +-- +-- Since 0.8.0.0 (type changed) +{-# INLINE sLength #-} +sLength :: (Dom f a, SingI n) => Sized f n a -> SNat n sLength = S.sLength @Nat +-- | Test if the sequence is empty or not. +-- +-- Since 0.7.0.0 +{-# INLINE null #-} null :: (Dom f a, CFoldable f) => Sized f n a -> Bool null = S.null @Nat +-------------------------------------------------------------------------------- +--- Indexing +-------------------------------------------------------------------------------- + +-- | (Unsafe) indexing with @Int@s. +-- If you want to check boundary statically, use '%!!' or 'sIndex'. +-- +-- Since 0.7.0.0 +{-# INLINE (!!) #-} (!!) :: (Dom f a, CFoldable f, (One <= m) ~ 'True) => Sized f m a -> Int -> a (!!) = (S.!!) @Nat +-- | Safe indexing with 'Ordinal's. +-- +-- Since 0.7.0.0 +{-# INLINE (%!!) #-} (%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c (%!!) = (S.%!!) @Nat +-- | Flipped version of '!!'. +-- +-- Since 0.7.0.0 +{-# INLINE index #-} index :: (Dom f a, CFoldable f, (One <= m) ~ 'True) => Int -> Sized f m a -> a index = S.index @Nat +-- | Flipped version of '%!!'. +-- +-- Since 0.7.0.0 +{-# INLINE sIndex #-} sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c sIndex = S.sIndex @Nat +-- | 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.7.0.0 +{-# INLINE head #-} head :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a head = S.head @Nat +-- | 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.7.0.0 +{-# INLINE last #-} last :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a last = S.last @Nat +-- | 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.7.0.0 +{-# INLINE uncons #-} uncons :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True) => Sized f n a -> Uncons f n a uncons = S.uncons @Nat +-- | 'uncons' with explicit specified length @n@ +-- +-- Since 0.7.0.0 +{-# INLINE uncons' #-} uncons' :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True) => Sized f n a -> Uncons f n a uncons' = S.uncons @Nat +-- | 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.7.0.0 +{-# INLINE unsnoc #-} unsnoc :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True) => Sized f n a -> Unsnoc f n a unsnoc = S.unsnoc @Nat +-- | 'unsnoc'' with explicit specified length @n@ +-- +-- Since 0.7.0.0 +{-# INLINE unsnoc' #-} unsnoc' :: (Dom f a, SingI n, CFreeMonoid f) => proxy n -> Sized f ('S n) a -> Unsnoc f ('S n) a unsnoc' = S.unsnoc' @Nat @@ -152,186 +242,453 @@ => Sized f n1 a -> a -> Unsnoc f n a pattern Unsnoc xs x = S.Unsnoc xs x +-- | 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.7.0.0 +{-# INLINE tail #-} tail :: (Dom f a, CFreeMonoid f) => Sized f (One + n) a -> Sized f n a tail = S.tail @Nat + +-- | 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.7.0.0 +{-# INLINE init #-} init :: (Dom f a, CFreeMonoid f) => Sized f (n + One) a -> Sized f n a init = S.init @Nat +-- | @take k xs@ takes first @k@ element of @xs@ where +-- the length of @xs@ should be larger than @k@. +-- +-- Since 0.7.0.0 +{-# INLINE take #-} take :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> Sized f n a take = S.take @Nat +-- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@. +-- +-- Since 0.7.0.0 +{-# INLINE takeAtMost #-} takeAtMost :: (Dom f a, CFreeMonoid f) => SNat n -> Sized f m a -> Sized f (Min n m) a takeAtMost = S.takeAtMost @Nat +-- | @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@. +-- +-- Since 0.7.0.0 +{-# INLINE drop #-} drop :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> Sized f (m - n) a drop = S.drop @Nat +-- | @splitAt k xs@ split @xs@ at @k@, where +-- the length of @xs@ should be less than or equal to @k@. +-- +-- Since 0.7.0.0 +{-# INLINE splitAt #-} splitAt :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a) splitAt = S.splitAt @Nat +-- | @splitAtMost k xs@ split @xs@ at @k@. +-- If @k@ exceeds the length of @xs@, then the second result value become empty. +-- +-- Since 0.7.0.0 +{-# INLINE splitAtMost #-} splitAtMost :: (Dom f a, CFreeMonoid f) => SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a) splitAtMost = S.splitAtMost @Nat +-------------------------------------------------------------------------------- +-- Construction +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Initialisation +-------------------------------------------------------------------------------- + +-- | Empty sequence. +-- +-- Since 0.7.0.0 (type changed) +{-# INLINE empty #-} empty :: (Dom f a, Monoid (f a)) => Sized f 'Z a empty = S.empty @Nat +-- | Sequence with one element. +-- +-- Since 0.7.0.0 +{-# INLINE singleton #-} singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f One a singleton = S.singleton @Nat +-- | Consruct the 'Sized' sequence from base type, but +-- the length parameter is dynamically determined and +-- existentially quantified; see also 'SomeSized''. +-- +-- Since 0.7.0.0 +{-# INLINE toSomeSized #-} toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a toSomeSized = S.toSomeSized @Nat +-- | Replicates the same value. +-- +-- Since 0.7.0.0 +{-# INLINE replicate #-} replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a replicate = S.replicate @Nat +-- | 'replicate' with the length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE replicate' #-} replicate' :: (Dom f a, CFreeMonoid f, SingI n) => a -> Sized f n a replicate' = S.replicate' @Nat +-- | Construct a sequence of the given length by applying the function to each index. +-- +-- Since 0.7.0.0 +{-# INLINE generate #-} generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a generate = S.generate @Nat +-- | 'generate' with length inferred. +-- +-- Since 0.8.0.0 +{-# INLINE generate' #-} +generate' :: forall f n a. + (SingI n, Dom f a, CFreeMonoid f) + => (Ordinal n -> a) -> Sized f n a +generate' = S.generate' @Nat + +-------------------------------------------------------------------------------- +--- Concatenation +-------------------------------------------------------------------------------- + +-- | Append an element to the head of sequence. +-- +-- Since 0.7.0.0 +{-# INLINE cons #-} cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a cons = S.cons @Nat +-- | Append an element to the tail of sequence. +-- +-- Since 0.7.0.0 +{-# INLINE snoc #-} snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a snoc = S.snoc @Nat +-- | Infix version of 'snoc'. +-- +-- Since 0.7.0.0 +{-# INLINE (<|) #-} (<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a (<|) = (S.<|) @Nat +-- | Append an element to the tail of sequence. +-- +-- Since 0.7.0.0 +{-# INLINE (|>) #-} (|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a (|>) = (S.|>) @Nat +-- | Infix version of 'append'. +-- +-- Since 0.7.0.0 +{-# INLINE (++) #-} (++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a (++) = (S.++) @Nat +-- | Append two lists. +-- +-- Since 0.7.0.0 +{-# INLINE append #-} append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a append = S.append @Nat +-- | Concatenates multiple sequences into one. +-- +-- Since 0.7.0.0 +{-# INLINE concat #-} concat :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a), CFreeMonoid f, CFunctor f', CFoldable f' ) => Sized f' m (Sized f n a) -> Sized f (m * n) a concat = S.concat @Nat +-------------------------------------------------------------------------------- +--- Zips +-------------------------------------------------------------------------------- + +-- | Zipping two sequences. Length is adjusted to shorter one. +-- +-- Since 0.7.0.0 +{-# INLINE zip #-} zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f) => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) zip = S.zip @Nat +-- | 'zip' for the sequences of the same length. +-- +-- Since 0.7.0.0 +{-# INLINE zipSame #-} zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f) => Sized f n a -> Sized f n b -> Sized f n (a, b) zipSame = S.zipSame @Nat +-- | Zipping two sequences with funtion. Length is adjusted to shorter one. +-- +-- Since 0.7.0.0 +{-# INLINE zipWith #-} zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c zipWith = S.zipWith @Nat +-- | 'zipWith' for the sequences of the same length. +-- +-- Since 0.7.0.0 +{-# INLINE zipWithSame #-} zipWithSame :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c zipWithSame = S.zipWithSame @Nat +-- | Unzipping the sequence of tuples. +-- +-- Since 0.7.0.0 +{-# INLINE unzip #-} unzip :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f) => Sized f n (a, b) -> (Sized f n a, Sized f n b) unzip = S.unzip @Nat +-- | Unzipping the sequence of tuples. +-- +-- Since 0.7.0.0 +{-# INLINE unzipWith #-} unzipWith :: (Dom f a, Dom f b, Dom f c, CUnzip f) => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c) unzipWith = S.unzipWith @Nat +-------------------------------------------------------------------------------- +-- Transformation +-------------------------------------------------------------------------------- + +-- | Map function. +-- +-- Since 0.7.0.0 +{-# INLINE map #-} map :: (Dom f a, Dom f b, CFreeMonoid f) => (a -> b) -> Sized f n a -> Sized f n b map = S.map @Nat +-- | Reverse function. +-- +-- Since 0.7.0.0 +{-# INLINE reverse #-} reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a reverse = S.reverse @Nat +-- | Intersperces. +-- +-- Since 0.7.0.0 +{-# INLINE intersperse #-} intersperse :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ((Two * n) -. One) a intersperse = S.intersperse @Nat +-- | Remove all duplicates. +-- +-- Since 0.7.0.0 +{-# INLINE nub #-} nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a nub = S.nub @Nat +-- | Sorting sequence by ascending order. +-- +-- Since 0.7.0.0 +{-# INLINE sort #-} sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a sort = S.sort @Nat +-- | Generalized version of 'sort'. +-- +-- Since 0.7.0.0 +{-# INLINE sortBy #-} sortBy :: (Dom f a, CFreeMonoid f) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a sortBy = S.sortBy @Nat +-- | Insert new element into the presorted sequence. +-- +-- Since 0.7.0.0 +{-# INLINE insert #-} insert :: (Dom f a, CFreeMonoid f, Ord a) => a -> Sized f n a -> Sized f ('S n) a insert = S.insert @Nat +-- | Generalized version of 'insert'. +-- +-- Since 0.7.0.0 +{-# INLINE insertBy #-} insertBy :: (Dom f a, CFreeMonoid f) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f ('S n) a insertBy = S.insertBy @Nat +-------------------------------------------------------------------------------- +-- Conversion +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- List +-------------------------------------------------------------------------------- + +-- | Convert to list. +-- +-- Since 0.7.0.0 +{-# INLINE toList #-} toList :: (Dom f a, CFoldable f) => Sized f n a -> [a] toList = S.toList @Nat +-- | 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.7.0.0 (type changed) +{-# INLINE fromList #-} fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a) fromList = S.fromList @Nat +-- | 'fromList' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE fromList' #-} fromList' :: (Dom f a, CFreeMonoid f, SingI n) => [a] -> Maybe (Sized f n a) fromList' = S.fromList' @Nat +-- | Unsafe version of 'fromList'. If the length of the given list does not +-- equal to @n@, then something unusual happens. +-- +-- Since 0.7.0.0 +{-# INLINE unsafeFromList #-} unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a unsafeFromList = S.unsafeFromList @Nat +-- | 'unsafeFromList' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE unsafeFromList' #-} unsafeFromList' :: (Dom f a, SingI n, CFreeMonoid f) => [a] -> Sized f n a unsafeFromList' = S.unsafeFromList' @Nat +-- | Construct a @Sized f n a@ by padding default value if the given list is short. +-- +-- Since 0.5.0.0 (type changed) +{-# INLINE fromListWithDefault #-} fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a fromListWithDefault = S.fromListWithDefault @Nat +-- | 'fromListWithDefault' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE fromListWithDefault' #-} fromListWithDefault' :: (Dom f a, SingI n, CFreeMonoid f) => a -> [a] -> Sized f n a fromListWithDefault' = S.fromListWithDefault' @Nat +-------------------------------------------------------------------------------- +--- Base containes +-------------------------------------------------------------------------------- + +-- | Forget the length and obtain the wrapped base container. +-- +-- Since 0.7.0.0 +{-# INLINE unsized #-} unsized :: Sized f n a -> f a unsized = S.unsized @Nat +-- | 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.7.0.0 +{-# INLINE toSized #-} toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a) toSized = S.toSized @Nat +-- | 'toSized' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE toSized' #-} toSized' :: (Dom f a, CFreeMonoid f, SingI n) => f a -> Maybe (Sized f n a) toSized' = S.toSized' @Nat +-- | Unsafe version of 'toSized'. If the length of the given list does not +-- equal to @n@, then something unusual happens. +-- +-- Since 0.7.0.0 +{-# INLINE unsafeToSized #-} unsafeToSized :: SNat n -> f a -> Sized f n a unsafeToSized = S.unsafeToSized @Nat +-- | 'unsafeToSized' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE unsafeToSized' #-} unsafeToSized' :: (Dom f a, SingI n) => f a -> Sized f n a unsafeToSized' = S.unsafeToSized' @Nat +-- | Construct a @Sized f n a@ by padding default value if the given list is short. +-- +-- Since 0.7.0.0 +{-# INLINE toSizedWithDefault #-} toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a toSizedWithDefault = S.toSizedWithDefault @Nat +-- | 'toSizedWithDefault' with the result length inferred. +-- +-- Since 0.7.0.0 +{-# INLINE toSizedWithDefault' #-} toSizedWithDefault' :: (Dom f a, SingI n, CFreeMonoid f) => a -> f a -> Sized f n a toSizedWithDefault' = S.toSizedWithDefault' @Nat +-------------------------------------------------------------------------------- +-- Querying +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Partitioning +-------------------------------------------------------------------------------- + +-- | 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.7.0.0 type Partitioned f (n :: Nat) a = S.Partitioned f n a pattern Partitioned @@ -342,68 +699,270 @@ {-# COMPLETE Partitioned #-} pattern Partitioned ls l rs r = S.Partitioned ls l rs r +-- | Take the initial segment as long as elements satisfys the predicate. +-- +-- Since 0.7.0.0 +{-# INLINE takeWhile #-} takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a takeWhile = S.takeWhile @Nat +-- | Drop the initial segment as long as elements satisfys the predicate. +-- +-- Since 0.7.0.0 +{-# INLINE dropWhile #-} dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a dropWhile = S.dropWhile @Nat +-- | Split the sequence into the longest prefix +-- of elements that satisfy the predicate +-- and the rest. +-- +-- Since 0.7.0.0 +{-# INLINE span #-} span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a span = S.span @Nat + +-- | Split the sequence into the longest prefix +-- of elements that do not satisfy the +-- predicate and the rest. +-- +-- Since 0.7.0.0 +{-# INLINE break #-} break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a break = S.break @Nat +-- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't. +-- +-- Since 0.7.0.0 +{-# INLINE partition #-} partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a partition = S.partition @Nat +-------------------------------------------------------------------------------- +--- Searching +-------------------------------------------------------------------------------- +-- | Membership test; see also 'notElem'. +-- +-- Since 0.7.0.0 +{-# INLINE elem #-} elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool elem = S.elem @Nat +-- | Negation of 'elem'. +-- +-- Since 0.7.0.0 +{-# INLINE notElem #-} notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool notElem = S.notElem @Nat +-- | Find the element satisfying the predicate. +-- +-- Since 0.7.0.0 +{-# INLINE find #-} find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a find = S.find @Nat +-- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists. +-- +-- Since 0.7.0.0 +{-# INLINE findIndex #-} findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int findIndex = S.findIndex @Nat +-- | 'Ordinal' version of 'findIndex'. +-- +-- Since 0.7.0.0 +{-# INLINE sFindIndex #-} sFindIndex :: (Dom f a, SingI n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) sFindIndex = S.sFindIndex @Nat +-- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices. +-- +-- Since 0.7.0.0 +{-# INLINE findIndices #-} findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int] findIndices = S.findIndices @Nat +-- | 'Ordinal' version of 'findIndices'. +-- +-- Since 0.7.0.0 +{-# INLINE sFindIndices #-} sFindIndices :: (Dom f a, CFoldable f, SingI n) => (a -> Bool) -> Sized f n a -> [Ordinal n] sFindIndices = S.sFindIndices @Nat -elemIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int -elemIndex = S.findIndex @Nat +-- | Returns the index of the given element in the list, if exists. +-- +-- Since 0.7.0.0 +{-# INLINE elemIndex #-} +elemIndex :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Maybe Int +elemIndex = S.elemIndex @Nat -sUnsafeElemIndex :: (Dom f a, SingI n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n) +sElemIndex, sUnsafeElemIndex :: (Dom f a, SingI n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n) {-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-} + +-- | Ordinal version of 'elemIndex'. +-- Since 0.7.0.0, we no longer do boundary check inside the definition. +-- +-- Since 0.7.0.0 sUnsafeElemIndex = S.sElemIndex @Nat -sElemIndex :: (Dom f a, SingI n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) -sElemIndex = S.sFindIndex @Nat +-- | Ordinal version of 'elemIndex'. +-- Since 0.7.0.0, we no longer do boundary check inside the definition. +-- +-- Since 0.7.0.0 +sElemIndex = S.sElemIndex @Nat -elemIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int] -elemIndices = S.findIndices @Nat +-- | Returns all indices of the given element in the list. +-- +-- Since 0.8.0.0 +{-# INLINE elemIndices #-} +elemIndices :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> [Int] +elemIndices = S.elemIndices @Nat -sElemIndices :: (Dom f a, CFoldable f, SingI n) => (a -> Bool) -> Sized f n a -> [Ordinal n] -sElemIndices = S.sFindIndices @Nat +-- | Ordinal version of 'elemIndices' +-- +-- Since 0.8.0.0 +{-# INLINE sElemIndices #-} +sElemIndices + :: (Dom f a, CFoldable f, SingI n, Eq a) + => a -> Sized f n a -> [Ordinal n] +sElemIndices = S.sElemIndices @Nat + +-------------------------------------------------------------------------------- +-- Views and Patterns +-------------------------------------------------------------------------------- + +{-$ViewsAndPatterns #ViewsAndPatterns# + + With GHC's @ViewPatterns@ and @PatternSynonym@ extensions, + we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor. + Curretnly, there are two direction view and patterns: Cons and Snoc. + Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead' + (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on + cons (resp. snoc) of @Sized f n a@ in O(1). +-} + +{-$views #views# + + With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows: + +@ +slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n +slen ('viewCons' -> 'NilCV') = 'SZ' +slen ('viewCons' -> _ ':-' as) = 'SS' (slen as) +slen _ = error "impossible" +@ + + The constraint @('KnownNat' n, 'Dom f 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 :: ('KnownNat' n, 'Dom f 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.7.0.0 type ConsView f (n :: Nat) a = S.ConsView f n a +-- | Since 0.8.0.0 +pattern NilCV + :: forall (f :: Type -> Type) n a. () + => (n ~ 'Z) + => ConsView f n a +pattern NilCV = S.NilCV + +-- | Since 0.8.0.0 +pattern (:-) + :: forall (f :: Type -> Type) n a. () + => forall n1. (n ~ (One + n1), SingI n1) + => a -> Sized f n1 a -> ConsView f n a +pattern l :- ls = l S.:- ls + +infixr 9 :- +{-# COMPLETE NilCV, (:-) #-} + +-- | Case analysis for the cons-side of sequence. +-- +-- Since 0.5.0.0 (type changed) viewCons :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a viewCons = S.viewCons @Nat +-- | View of the left end of sequence (snoc-side). +-- +-- Since 0.7.0.0 type SnocView f (n :: Nat) a = S.SnocView f n a +-- | Since 0.8.0.0 +pattern NilSV + :: forall (f :: Type -> Type) n a. () + => (n ~ 'Z) + => SnocView f n a +pattern NilSV = S.NilSV + +infixl 9 :-:: +-- | Since 0.8.0.0 +pattern (:-::) + :: forall (f :: Type -> Type) n a. () + => forall n1. (n ~ (n1 + One), SingI n1) + => Sized f n1 a -> a -> SnocView f n a +pattern ls :-:: l = ls S.:-:: l +{-# COMPLETE NilSV, (:-::) #-} + +-- | Case analysis for the snoc-side of sequence. +-- +-- Since 0.8.0.0 (type changed) viewSnoc :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a viewSnoc = S.viewCons @Nat + +{-$patterns #patterns# + + So we can pattern match on both end of sequence via views, but + it is rather clumsy to nest it. For example: + +@ +nextToHead :: ('Dom f 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 :: ('Dom f 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, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n +slen 'Nil' = 'SZ' +slen (_ ':<' as) = 'SS' (slen as) +slen _ = error "impossible" +@ + + So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to + pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. + @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors, + but pattern synonyms so we cannot use them in expression contexts. + For more detail on pattern synonyms, see + + and + . +-} + +-- | Pattern synonym for cons-side uncons. pattern (:<) :: forall (f :: Type -> Type) a (n :: Nat). (Dom f a, SingI n, CFreeMonoid f) @@ -412,11 +971,20 @@ pattern a :< b = a S.:< b infixr 5 :< +-- | Pattern synonym for a nil sequence. +pattern Nil + :: forall (f :: Type -> Type) a n. + (Dom f a, SingI n, CFreeMonoid f) + => (n ~ 'Z) => Sized f n a +pattern Nil = S.Nil + +-- | Pattern synonym for cons-side nil. pattern NilL :: forall f (n :: Nat) a. (SingI n, CFreeMonoid f, Dom f a) => n ~ 'Z => Sized f n a -pattern NilL = S.NilL +pattern NilL = Nil +-- | Pattern synonym for snoc-side unsnoc. pattern (:>) :: forall (f :: Type -> Type) a (n :: Nat). (Dom f a, SingI n, CFreeMonoid f) @@ -425,7 +993,14 @@ pattern a :> b = a S.:> b infixl 5 :> +-- | Pattern synonym for snoc-side nil. pattern NilR :: forall f (n :: Nat) a. (CFreeMonoid f, Dom f a, SingI n) => n ~ 'Z => Sized f n a -pattern NilR = S.NilR +pattern NilR = Nil +{-# COMPLETE (:<), NilL #-} +{-# COMPLETE (:<), NilR #-} +{-# COMPLETE (:<), Nil #-} +{-# COMPLETE (:>), NilL #-} +{-# COMPLETE (:>), NilR #-} +{-# COMPLETE (:>), Nil #-} diff --git a/test/opt-test.hs b/test/opt-test.hs --- a/test/opt-test.hs +++ b/test/opt-test.hs @@ -16,6 +16,7 @@ import qualified Data.Vector.Storable as S import Data.Vector.Unboxed (Unbox) import qualified Data.Vector.Unboxed as U +import Numeric.Natural (Natural) import Shared import Test.Hspec import Test.Inspection @@ -79,6 +80,12 @@ zipWith_Boxed :: (a -> b -> c) -> V.Vector a -> V.Vector b -> V.Vector c zipWith_Boxed = V.zipWith +length_two :: Dom f a => Sized f 2 a -> Int +length_two = SV.length + +const_two_dom :: Dom f a => Sized f 2 a -> Int +const_two_dom = const 2 + main :: IO () main = hspec $ do describe "czipWith" $ do @@ -108,11 +115,6 @@ $ 'zipWithSame_Boxed `hasNoTypeClassesExcept` [''G.Vector] ) - it "doesn't contain type classes, if fully instantiated" $ - checkInspection - $(inspectTest - $ hasNoTypeClasses 'zipWithSame_Boxed_mono - ) it "is almost the same as the original zipWith (Boxed)" $ checkInspection $(inspectTest $ @@ -136,3 +138,17 @@ 'zipWithSame_Unboxed_monomorphic ==- 'zipWith_Unboxed_monomorphic ) + describe "length" $ do + it "is a constant function when length is concrete (with Dom dictionary)" $ + checkInspection + $(inspectTest $ + 'length_two ==- 'const_two_dom + ) + it "doesn't contain Integer when the length is concrete" $ + checkInspection + $(inspectTest $ hasNoType 'length_two ''Integer + ) + it "doesn't contain Natural when the length is concrete" $ + checkInspection + $(inspectTest $ hasNoType 'length_two ''Natural + )