packages feed

vec (empty) → 0

raw patch · 10 files changed

+2063/−0 lines, 10 filesdep +adjunctionsdep +basedep +base-compatsetup-changed

Dependencies added: adjunctions, base, base-compat, boring, criterion, deepseq, distributive, fin, hashable, inspection-testing, lens, semigroupoids, semigroups, tagged, vec, vector

Files

+ ChangeLog.md view
@@ -0,0 +1,4 @@+# Revision history for boring+## 0++- First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2017, Oleg Grenrus++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Oleg Grenrus nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ bench/Bench.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE GADTs #-}+module Main (main) where++import Criterion.Main++import Data.Fin      (Fin (..))+import Data.Type.Nat (Nat5)+import Data.Vec.Lazy (Vec (..))++import qualified Data.Vec.Pull       as P+import qualified Data.Vector         as V+import qualified Data.Vector.Unboxed as U++import DotProduct++xsl, ysl :: [Int]+xsl = [1,2,3,4,5]+ysl = [6,7,8,9,0]++xsv, ysv :: V.Vector Int+xsv = V.fromList xsl+ysv = V.fromList ysl++xsu, ysu :: U.Vector Int+xsu = U.fromList xsl+ysu = U.fromList ysl++xs, ys :: Vec Nat5 Int+xs = 1 ::: 2 ::: 3 ::: 4 ::: 5 ::: VNil+ys = 6 ::: 7 ::: 8 ::: 9 ::: 0 ::: VNil++xsp, ysp :: P.Vec Nat5 Int+xsp = P.Vec $ \i -> case i of+    Z               -> 1+    S Z             -> 2+    S (S Z)         -> 3+    S (S (S Z))     -> 4+    S (S (S (S Z))) -> 5+ysp = P.Vec $ \i -> case i of+    Z               -> 6+    S Z             -> 7+    S (S Z)         -> 8+    S (S (S Z))     -> 9+    S (S (S (S Z))) -> 0++main :: IO ()+main = defaultMain+    [ bgroup "dot product"+        [ bench "list"    $ whnf (uncurry listDotProduct)    (xsl, ysl)+        , bench "vector"  $ whnf (uncurry vectorDotProduct)  (xsv, ysv)+        , bench "unboxed" $ whnf (uncurry unboxedDotProduct) (xsu, ysu)+        , bench "vec"     $ whnf (uncurry vecDotProduct)     (xs,  ys)+        , bench "pull"    $ whnf (uncurry pullDotProduct)    (xs,  ys)+        , bench "pull'"   $ whnf (uncurry pullDotProduct')   (xsp, ysp)+        , bench "inline"  $ whnf (uncurry inlineDotProduct)  (xs,  ys)+        ]+    ]
+ bench/DotProduct.hs view
@@ -0,0 +1,29 @@+module DotProduct where++import qualified Data.Type.Nat        as N+import qualified Data.Vec.Lazy        as L+import qualified Data.Vec.Lazy.Inline as I+import qualified Data.Vec.Pull        as P+import qualified Data.Vector          as V+import qualified Data.Vector.Unboxed  as U++listDotProduct :: [Int] -> [Int] -> Int+listDotProduct xs ys = sum (zipWith (*) xs ys)++vectorDotProduct :: V.Vector Int -> V.Vector Int -> Int+vectorDotProduct xs ys = V.sum (V.zipWith (*) xs ys)++unboxedDotProduct :: U.Vector Int -> U.Vector Int -> Int+unboxedDotProduct xs ys = U.sum (U.zipWith (*) xs ys)++vecDotProduct :: L.Vec n Int -> L.Vec n Int -> Int+vecDotProduct xs ys = L.sum (L.zipWith (*) xs ys)++pullDotProduct :: N.SNatI n => L.Vec n Int -> L.Vec n Int -> Int+pullDotProduct xs ys = pullDotProduct' (L.toPull xs) (L.toPull ys)++pullDotProduct' :: N.SNatI n => P.Vec n Int -> P.Vec n Int -> Int+pullDotProduct' xs ys = P.sum (P.zipWith (*) xs ys)++inlineDotProduct :: N.InlineInduction n => L.Vec n Int -> L.Vec n Int -> Int+inlineDotProduct xs ys = I.sum (I.zipWith (*) xs ys)
+ src/Data/Vec/Lazy.hs view
@@ -0,0 +1,731 @@+{-# LANGUAGE BangPatterns           #-}+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE DeriveDataTypeable     #-}+{-# LANGUAGE EmptyCase              #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE KindSignatures         #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE StandaloneDeriving     #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE UndecidableInstances   #-}+-- | Lazy length-indexed list: 'Vec'.+module Data.Vec.Lazy (+    Vec (..),+    -- * Construction+    empty,+    singleton,+    withDict,+    -- * Conversions+    toPull,+    fromPull,+    _Pull,+    toList,+    fromList,+    _Vec,+    fromListPrefix,+    reifyList,+    -- * Indexing+    (!),+    ix,+    _Cons,+    _head,+    _tail,+    cons,+    head,+    tail,+    -- * Concatenation and splitting+    (++),+    split,+    concatMap,+    concat,+    chunks,+    -- * Folds+    foldMap,+    foldMap1,+    ifoldMap,+    ifoldMap1,+    foldr,+    ifoldr,+    foldl',+    -- * Special folds+    length,+    null,+    sum,+    product,+    -- * Mapping+    map,+    imap,+    traverse,+    traverse1,+    itraverse,+    itraverse_,+    -- * Zipping+    zipWith,+    izipWith,+    -- * Monadic+    bind,+    join,+    -- * Universe+    universe,+    -- * VecEach+    VecEach (..),+    )  where++import Prelude ()+import Prelude.Compat+       (Bool (..), Eq (..), Functor (..), Int, Maybe (..),+       Monad (..), Monoid (..), Num (..), Ord (..), Show (..), id, seq,+       showParen, showString, ($), (.), (<$>))++import Control.Applicative (Applicative (..))+import Control.DeepSeq     (NFData (..))+import Control.Lens        ((<&>))+import Data.Boring         (Boring (..))+import Data.Distributive   (Distributive (..))+import Data.Fin            (Fin)+import Data.Functor.Apply  (Apply (..))+import Data.Functor.Rep    (Representable (..), distributeRep)+import Data.Hashable       (Hashable (..))+import Data.Nat+import Data.Semigroup      (Semigroup (..))+import Data.Typeable       (Typeable)++--- Instances+import qualified Control.Lens               as I+import qualified Data.Foldable              as I (Foldable (..))+import qualified Data.Functor.Bind          as I (Bind (..))+import qualified Data.Semigroup.Foldable    as I (Foldable1 (..))+import qualified Data.Semigroup.Traversable as I (Traversable1 (..))+import qualified Data.Traversable           as I (Traversable (..))++import qualified Data.Fin      as F+import qualified Data.Type.Nat as N+import qualified Data.Vec.Pull as P++infixr 5 :::++-- | Vector, i.e. length-indexed list.+data Vec (n :: Nat) a where+    VNil  :: Vec 'Z a+    (:::) :: a -> Vec n a -> Vec ('S n) a+  deriving (Typeable)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++deriving instance Eq a => Eq (Vec n a)+deriving instance Ord a => Ord (Vec n a)++instance Show a => Show (Vec n a) where+    showsPrec _ VNil       = showString "VNil"+    showsPrec d (x ::: xs) = showParen (d > 5)+        $ showsPrec 6 x+        . showString " ::: "+        . showsPrec 5 xs++instance Functor (Vec n) where+    fmap = map++instance I.Foldable (Vec n) where+    foldMap = foldMap++    foldr  = foldr+    foldl' = foldl'++#if MIN_VERSION_base(4,8,0)+    null    = null+    length  = length+    sum     = sum+    product = product+#endif++instance n ~ 'S m => I.Foldable1 (Vec n) where+    foldMap1 = foldMap1++instance I.Traversable (Vec n) where+    traverse = traverse++instance n ~ 'S m => I.Traversable1 (Vec n) where+    traverse1 = traverse1++instance NFData a => NFData (Vec n a) where+    rnf VNil       = ()+    rnf (x ::: xs) = rnf x `seq` rnf xs++instance Hashable a => Hashable (Vec n a) where+    hashWithSalt salt VNil = hashWithSalt salt (0 :: Int)+    hashWithSalt salt (x ::: xs) = salt+        `hashWithSalt` x+        `hashWithSalt` xs++instance N.SNatI n => Applicative (Vec n) where+    pure x = N.induction1 VNil (x :::)+    (<*>)  = zipWith ($)+    _ *> x = x+    x <* _ = x+#if MIN_VERSION_base(4,10,0)+    liftA2 = zipWith+#endif++instance N.SNatI n => Monad (Vec n) where+    return = pure+    (>>=)  = bind+    _ >> x = x++instance N.SNatI n => Distributive (Vec n) where+    distribute = distributeRep++instance N.SNatI n => Representable (Vec n) where+    type Rep (Vec n) = Fin n+    tabulate = fromPull . tabulate+    index    = index . toPull++instance Semigroup a => Semigroup (Vec n a) where+    (<>) = zipWith (<>)++instance (Monoid a, N.SNatI n) => Monoid (Vec n a) where+    mempty = pure mempty+    mappend = zipWith mappend++instance n ~ 'N.Z => Boring (Vec n a) where+    boring = VNil++instance Apply (Vec n) where+    (<.>) = zipWith ($)+    _ .> x = x+    x <. _ = x++instance I.Bind (Vec n) where+    (>>-) = bind+    join  = join++instance I.FunctorWithIndex (Fin n) (Vec n) where+    imap = imap++instance I.FoldableWithIndex (Fin n) (Vec n) where+    ifoldMap = ifoldMap+    ifoldr   = ifoldr++instance I.TraversableWithIndex (Fin n) (Vec n) where+    itraverse = itraverse++instance I.Each (Vec n a) (Vec n b) a b where+    each = traverse++type instance I.Index (Vec n a)   = Fin n+type instance I.IxValue (Vec n a) = a++-- | 'Vec' doesn't have 'I.At' instance, as we __cannot__ remove value from 'Vec'.+-- See 'ix' in "Data.Vec.Lazy" module for an 'I.Lens' (not 'I.Traversal').+instance I.Ixed (Vec n a) where+    ix = ix++instance I.Field1 (Vec ('S n) a) (Vec ('S n) a) a a where+    _1 = _head++instance I.Field2 (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a where+    _2 = _tail . _head++instance I.Field3 (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a where+    _3 = _tail . _tail . _head++instance I.Field4 (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a where+    _4 = _tail . _tail . _tail . _head++instance I.Field5 (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S ('S n))))) a) a a where+    _5 = _tail . _tail . _tail . _tail . _head++instance I.Field6 (Vec ('S ('S ('S ('S ('S ('S n)))))) a) (Vec ('S ('S ('S ('S ('S ('S n)))))) a) a a where+    _6 = _tail . _tail . _tail . _tail . _tail . _head++instance I.Field7 (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) a a where+    _7 = _tail . _tail . _tail . _tail . _tail . _tail . _head++instance I.Field8 (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) a a where+    _8 = _tail . _tail . _tail . _tail . _tail . _tail . _tail . _head++instance I.Field9 (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) a a where+    _9 = _tail . _tail . _tail . _tail . _tail . _tail . _tail . _tail . _head++-------------------------------------------------------------------------------+-- Construction+-------------------------------------------------------------------------------++-- | Empty 'Vec'.+empty :: Vec 'Z a+empty = VNil++-- | 'Vec' with exactly one element.+--+-- >>> singleton True+-- True ::: VNil+--+singleton :: a -> Vec ('S 'Z) a+singleton x = x ::: VNil++-- | /O(n)/. Recover 'N.InlineInduction' (and 'N.SNatI') dictionary from a 'Vec' value.+--+-- Example: 'N.reflect' is constrained with @'N.SNatI' n@, but if we have a+-- @'Vec' n a@, we can recover that dictionary:+--+-- >>> let f :: forall n a. Vec n a -> N.Nat; f v = withDict v (N.reflect (Proxy :: Proxy n)) in f (True ::: VNil)+-- 1+--+-- /Note:/ using 'N.InlineInduction' will be suboptimal, as if GHC has no+-- opportunity to optimise the code, the recusion won't be unfold.+-- How bad such code will perform? I don't know, we'll need benchmarks.+--+withDict :: Vec n a -> (N.InlineInduction n => r) -> r+withDict VNil       r = r+withDict (_ ::: xs) r = withDict xs r++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Convert to pull 'P.Vec'.+toPull :: Vec n a -> P.Vec n a+toPull VNil       = P.Vec F.absurd+toPull (x ::: xs) = P.Vec $ \n -> case n of+    F.Z   -> x+    F.S m -> P.unVec (toPull xs) m++-- | Convert from pull 'P.Vec'.+fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a+fromPull (P.Vec f) = case N.snat :: N.SNat n of+    N.SZ -> VNil+    N.SS -> f F.Z ::: fromPull (P.Vec (f . F.S))++-- | An 'I.Iso' from 'toPull' and 'fromPull'.+_Pull :: N.SNatI n => I.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)+_Pull = I.iso toPull fromPull++-- | Convert 'Vec' to list.+--+-- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil+-- "foo"+toList :: Vec n a -> [a]+toList VNil       = []+toList (x ::: xs) = x : toList xs++-- | Convert list @[a]@ to @'Vec' n a@.+-- Returns 'Nothing' if lengths don't match exactly.+--+-- >>> fromList "foo" :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> fromList "quux" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+-- >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+fromList :: N.SNatI n => [a] -> Maybe (Vec n a)+fromList = getFromList (N.induction1 start step) where+    start :: FromList 'Z a+    start = FromList $ \xs -> case xs of+        []      -> Just VNil+        (_ : _) -> Nothing++    step :: FromList n a -> FromList ('N.S n) a+    step (FromList f) = FromList $ \xs -> case xs of+        []       -> Nothing+        (x : xs') -> (x :::) <$> f xs'++newtype FromList n a = FromList { getFromList :: [a] -> Maybe (Vec n a) }++-- | Prism from list.+--+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)+-- Nothing+--+-- >>> _Vec # (True ::: False ::: VNil)+-- [True,False]+--+_Vec :: N.SNatI n => I.Prism' [a] (Vec n a)+_Vec = I.prism' toList fromList++-- | Convert list @[a]@ to @'Vec' n a@.+-- Returns 'Nothing' if input list is too short.+--+-- >>> fromListPrefix "foo" :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> fromListPrefix "quux" :: Maybe (Vec N.Nat3 Char)+-- Just ('q' ::: 'u' ::: 'u' ::: VNil)+--+-- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)+fromListPrefix = getFromList (N.induction1 start step) where+    start :: FromList 'Z a+    start = FromList $ \_ -> Just VNil -- different than in fromList case++    step :: FromList n a -> FromList ('N.S n) a+    step (FromList f) = FromList $ \xs -> case xs of+        []       -> Nothing+        (x : xs') -> (x :::) <$> f xs'++-- | Reify any list @[a]@ to @'Vec' n a@.+--+-- >>> reifyList "foo" length+-- 3+reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r+reifyList []       f = f VNil+reifyList (x : xs) f = reifyList xs $ \xs' -> f (x ::: xs')++-------------------------------------------------------------------------------+-- Indexing+-------------------------------------------------------------------------------++-- | Indexing.+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! F.S F.Z+-- 'b'+--+(!) :: Vec n a -> Fin n -> a+(!) (x ::: _)  (F.Z)   = x+(!) (_ ::: xs) (F.S n) = xs ! n+(!) VNil n = case n of {}++-- | Index lens.+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)+-- 'b'+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ 'x'+-- 'a' ::: 'x' ::: 'c' ::: VNil+--+ix :: Fin n -> I.Lens' (Vec n a) a+ix F.Z     f (x ::: xs) = (::: xs) <$> f x+ix (F.S n) f (x ::: xs) = (x :::)  <$> ix n f xs++-- | Match on non-empty 'Vec'.+--+-- /Note:/ @lens@ 'I._Cons' is a 'I.Prism'.+-- In fact, @'Vec' n a@ cannot have an instance of 'I.Cons' as types don't match.+--+_Cons :: I.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)+_Cons = I.iso (\(x ::: xs) -> (x, xs)) (\(x, xs) -> x ::: xs)++-- | Head lens. /Note:/ @lens@ 'I._head' is a 'I.Traversal''.+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head+-- 'a'+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'+-- 'x' ::: 'b' ::: 'c' ::: VNil+--+_head :: I.Lens' (Vec ('S n) a) a+_head f (x ::: xs) = (::: xs) <$> f x+{-# INLINE head #-}++-- | Head lens. /Note:/ @lens@ 'I._head' is a 'I.Traversal''.+_tail :: I.Lens' (Vec ('S n) a) (Vec n a)+_tail f (x ::: xs) = (x :::) <$> f xs+{-# INLINE _tail #-}++-- | Cons an element in front of a 'Vec'.+cons :: a -> Vec n a -> Vec ('S n) a+cons = (:::)++-- | The first element of a 'Vec'.+head :: Vec ('S n) a -> a+head (x ::: _) = x++-- | The elements after the 'head' of a 'Vec'.+tail :: Vec ('S n) a -> Vec n a+tail (_ ::: xs) = xs++-------------------------------------------------------------------------------+-- Concatenation+-------------------------------------------------------------------------------++infixr 5 ++++-- | Append two 'Vec'.+--+-- >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)+-- 'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil+--+(++) :: Vec n a -> Vec m a -> Vec (N.Plus n m) a+VNil       ++ ys = ys+(x ::: xs) ++ ys = x ::: xs ++ ys++-- | Split vector into two parts. Inverse of '++'.+--+-- >>> split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)+-- ('a' ::: VNil,'b' ::: 'c' ::: VNil)+--+-- >>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))+-- 'a' ::: 'b' ::: 'c' ::: VNil+--+split :: N.SNatI n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)+split = appSplit (N.induction1 start step) where+    start :: Split m 'Z a+    start = Split $ \xs -> (VNil, xs)++    step :: Split m n a -> Split m ('S n) a+    step (Split f) = Split $ \(x ::: xs) -> case f xs of+        (ys, zs) -> (x ::: ys, zs)++newtype Split m n a = Split { appSplit :: Vec (N.Plus n m) a -> (Vec n a, Vec m a) }++-- | Map over all the elements of a 'Vec' and concatenate the resulting 'Vec's.+--+-- >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)+-- 'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil+--+concatMap :: (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b+concatMap _ VNil       = VNil+concatMap f (x ::: xs) = f x ++ concatMap f xs++-- | @'concatMap' 'id'@+concat :: Vec n (Vec m a) -> Vec (N.Mult n m) a+concat = concatMap id++-- | Inverse of 'concat'.+--+-- >>> chunks <$> fromListPrefix [1..] :: Maybe (Vec N.Nat2 (Vec N.Nat3 Int))+-- Just ((1 ::: 2 ::: 3 ::: VNil) ::: (4 ::: 5 ::: 6 ::: VNil) ::: VNil)+--+-- >>> let idVec x = x :: Vec N.Nat2 (Vec N.Nat3 Int)+-- >>> concat . idVec . chunks <$> fromListPrefix [1..]+-- Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)+--+chunks :: (N.SNatI n, N.SNatI m) => Vec (N.Mult n m) a -> Vec n (Vec m a)+chunks = getChunks $ N.induction1 start step where+    start :: Chunks m 'Z a+    start = Chunks $ \_ -> VNil++    step :: forall m n a. N.SNatI m => Chunks m n a -> Chunks m ('S n) a+    step (Chunks go) = Chunks $ \xs ->+        let (ys, zs) = split xs :: (Vec m a, Vec (N.Mult n m) a)+        in ys ::: go zs++newtype Chunks  m n a = Chunks  { getChunks  :: Vec (N.Mult n m) a -> Vec n (Vec m a) }++-------------------------------------------------------------------------------+-- Mapping+-------------------------------------------------------------------------------++-- | >>> map not $ True ::: False ::: VNil+-- False ::: True ::: VNil+--+map :: (a -> b) -> Vec n a -> Vec n b+map _ VNil       = VNil+map f (x ::: xs) = f x ::: fmap f xs++-- | >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil+-- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil+--+imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b+imap _ VNil       = VNil+imap f (x ::: xs) = f F.Z x ::: imap (f . F.S) xs++-- | Apply an action to every element of a 'Vec', yielding a 'Vec' of results.+traverse :: forall n f a b. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)+traverse f = go where+    go :: Vec m a -> f (Vec m b)+    go VNil       = pure VNil+    go (x ::: xs) = (:::) <$> f x <*> go xs++-- | Apply an action to non-empty 'Vec', yielding a 'Vec' of results.+traverse1 :: forall n f a b. Apply f => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)+traverse1 f = go where+    go :: Vec ('S m) a -> f (Vec ('S m) b)+    go (x ::: VNil)         = (::: VNil) <$> f x+    go (x ::: xs@(_ ::: _)) = (:::) <$> f x <.> go xs++-- | Apply an action to every element of a 'Vec' and its index, yielding a 'Vec' of results.+itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)+itraverse _ VNil       = pure VNil+itraverse f (x ::: xs) = (:::) <$> f F.Z x <*> I.itraverse (f . F.S) xs++-- | Apply an action to every element of a 'Vec' and its index, ignoring the results.+itraverse_ :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f ()+itraverse_ _ VNil       = pure ()+itraverse_ f (x ::: xs) = f F.Z x *> itraverse_ (f . F.S) xs++-------------------------------------------------------------------------------+-- Folding+-------------------------------------------------------------------------------++-- | See 'I.Foldable'.+foldMap :: Monoid m => (a -> m) -> Vec n a -> m+foldMap _ VNil       = mempty+foldMap f (x ::: xs) = mappend (f x) (foldMap f xs)++-- | See 'I.Foldable1'.+foldMap1 :: Semigroup s => (a -> s) -> Vec ('S n) a -> s+foldMap1 f (x ::: VNil)         = f x+foldMap1 f (x ::: xs@(_ ::: _)) = f x <> foldMap1 f xs++-- | See 'I.FoldableWithIndex'.+ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m+ifoldMap _ VNil       = mempty+ifoldMap f (x ::: xs) = mappend (f F.Z x) (ifoldMap (f . F.S) xs)++-- | There is no type-class for this :(+ifoldMap1 :: Semigroup s => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s+ifoldMap1 f (x ::: VNil)         = f F.Z x+ifoldMap1 f (x ::: xs@(_ ::: _)) = f F.Z x <> ifoldMap1 (f . F.S) xs++-- | Right fold.+foldr :: forall a b n. (a -> b -> b) -> b -> Vec n a -> b+foldr f z = go where+    go :: Vec m a -> b+    go VNil       = z+    go (x ::: xs) = f x (go xs)++-- | Right fold with an index.+ifoldr :: forall a b n. (Fin n -> a -> b -> b) -> b -> Vec n a -> b+ifoldr _ z VNil       = z+ifoldr f z (x ::: xs) = f F.Z x (ifoldr (f . F.S) z xs)++-- | Strict left fold.+foldl' :: forall a b n. (b -> a -> b) -> b -> Vec n a -> b+foldl' f z = go z where+    go :: b -> Vec m a -> b+    go !acc VNil       = acc+    go !acc (x ::: xs) = go (f acc x) xs++-- | Yield the length of a 'Vec'. /O(n)/+length :: Vec n a -> Int+length VNil = 0+length (_ ::: xs) = 1 + length xs++-- | Test whether a 'Vec' is empty. /O(1)/+null :: Vec n a -> Bool+null VNil      = True+null (_ ::: _) = False++-------------------------------------------------------------------------------+-- Special folds+-------------------------------------------------------------------------------++-- | Non-strict 'sum'.+sum :: Num a => Vec n a -> a+sum VNil       = 0+sum (x ::: xs) = x + sum xs++-- | Non-strict 'product'.+product :: Num a => Vec n a -> a+product VNil       = 1+product (x ::: xs) = x * sum xs++-------------------------------------------------------------------------------+-- Zipping+-------------------------------------------------------------------------------++-- | Zip two 'Vec's with a function.+zipWith ::  (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+zipWith _ VNil       VNil       = VNil+zipWith f (x ::: xs) (y ::: ys) = f x y ::: zipWith f xs ys++-- | Zip two 'Vec's. with a function that also takes the elements' indices.+izipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+izipWith _ VNil       VNil       = VNil+izipWith f (x ::: xs) (y ::: ys) = f F.Z x y ::: izipWith (f . F.S) xs ys++-------------------------------------------------------------------------------+-- Monadic+-------------------------------------------------------------------------------++-- | Monadic bind.+bind :: Vec n a -> (a -> Vec n b) -> Vec n b+bind VNil       _ = VNil+bind (x ::: xs) f = head (f x) ::: bind xs (tail . f)++-- | Monadic join.+--+-- >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil+-- 'a' ::: 'd' ::: VNil+join :: Vec n (Vec n a) -> Vec n a+join VNil       = VNil+join (x ::: xs) = head x ::: join (map tail xs)++-------------------------------------------------------------------------------+-- universe+-------------------------------------------------------------------------------++-- | Get all @'Fin' n@ in a @'Vec' n@.+--+-- >>> universe :: Vec N.Nat3 (Fin N.Nat3)+-- 0 ::: 1 ::: 2 ::: VNil+universe :: N.SNatI n => Vec n (Fin n)+universe = getUniverse (N.induction first step) where+    first :: Universe 'Z+    first = Universe VNil++    step :: Universe m -> Universe ('S m)+    step (Universe go) = Universe (F.Z ::: map F.S go)++newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }++-------------------------------------------------------------------------------+-- VecEach+-------------------------------------------------------------------------------++-- | Write functions on 'Vec'. Use them with tuples.+--+-- 'VecEach' can be used to avoid "this function won't change the length of the+-- list" in DSLs.+--+-- __bad:__ Instead of+--+-- @+-- [x, y] <- badDslMagic ["foo", "bar"]  -- list!+-- @+--+-- __good:__ we can write+--+-- @+-- (x, y) <- betterDslMagic ("foo", "bar") -- homogenic tuple!+-- @+--+-- where @betterDslMagic@ can be defined using 'traverseWithVec'.+--+class I.Each s t a b => VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where+    mapWithVec :: (forall n. N.InlineInduction n => Vec n a -> Vec n b) -> s -> t+    traverseWithVec :: Applicative f => (forall n. N.InlineInduction n => Vec n a -> f (Vec n b)) -> s -> f t++instance (a ~ a', b ~ b') => VecEach (a, a') (b, b') a b where+    mapWithVec f ~(x, y) = case f (x ::: y ::: VNil) of+        x' ::: y' ::: VNil -> (x', y')++    traverseWithVec f ~(x, y) = f (x ::: y ::: VNil) <&> \res -> case res of+        x' ::: y' ::: VNil -> (x', y')++instance (a ~ a2, a ~ a3, b ~ b2, b ~ b3) => VecEach (a, a2, a3) (b, b2, b3) a b where+    mapWithVec f ~(x, y, z) = case f (x ::: y ::: z ::: VNil) of+        x' ::: y' ::: z' ::: VNil -> (x', y', z')++    traverseWithVec f ~(x, y, z) = f (x ::: y ::: z ::: VNil) <&> \res -> case res of+        x' ::: y' ::: z' ::: VNil -> (x', y', z')++instance (a ~ a2, a ~ a3, a ~ a4, b ~ b2, b ~ b3, b ~ b4) => VecEach (a, a2, a3, a4) (b, b2, b3, b4) a b where+    mapWithVec f ~(x, y, z, u) = case f (x ::: y ::: z ::: u ::: VNil) of+        x' ::: y' ::: z' ::: u' ::: VNil -> (x', y', z', u')++    traverseWithVec f ~(x, y, z, u) = f (x ::: y ::: z ::: u ::: VNil) <&> \res -> case res of+        x' ::: y' ::: z' ::: u' ::: VNil -> (x', y', z', u')++-------------------------------------------------------------------------------+-- Doctest+-------------------------------------------------------------------------------++-- $setup+-- >>> :set -XScopedTypeVariables+-- >>> import Control.Lens ((^.), (&), (.~), (^?), (#))+-- >>> import Data.Proxy (Proxy (..))+-- >>> import Prelude.Compat (Char, not, uncurry)
+ src/Data/Vec/Lazy/Inline.hs view
@@ -0,0 +1,576 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE EmptyCase              #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE KindSignatures         #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE UndecidableInstances   #-}+-- | A variant of "Data.Vec.Lazy" with functions written using 'N.InlineInduction'.+-- The hypothesis is that these (goursive) functions could be fully unrolled,+-- if the 'Vec' size @n@ is known at compile time.+--+-- The module has the same API as "Data.Vec.Lazy" (sans 'L.withDict' and 'foldl'').+-- /Note:/ instance methods aren't changed, the 'Vec' type is the same.+module Data.Vec.Lazy.Inline (+    Vec (..),+    -- * Construction+    empty,+    singleton,+    -- * Conversions+    toPull,+    fromPull,+    _Pull,+    toList,+    fromList,+    _Vec,+    fromListPrefix,+    reifyList,+    -- * Indexing+    (!),+    ix,+    _Cons,+    _head,+    _tail,+    cons,+    head,+    tail,+    -- * Concatenation and splitting+    (++),+    split,+    concatMap,+    concat,+    chunks,+    -- * Folds+    foldMap,+    foldMap1,+    ifoldMap,+    ifoldMap1,+    foldr,+    ifoldr,+    -- * Special folds+    length,+    null,+    sum,+    product,+    -- * Mapping+    map,+    imap,+    traverse,+    traverse1,+    itraverse,+    itraverse_,+    -- * Zipping+    zipWith,+    izipWith,+    -- * Monadic+    bind,+    join,+    -- * Universe+    universe,+    -- * VecEach+    VecEach (..)+    )  where++import Prelude ()+import Prelude.Compat+       (Applicative (..), Int, Maybe (..), Monoid (..), Num (..), const, id,+       ($), (.), (<$>))++import Control.Applicative (liftA2)+import Data.Fin            (Fin)+import Data.Functor.Apply  (Apply, liftF2)+import Data.Nat+import Data.Semigroup      (Semigroup (..))+import Data.Vec.Lazy+       (Vec (..), VecEach (..), cons, empty, head, null, reifyList, singleton,+       tail, _Cons, _head, _tail)++--- Instances+import qualified Control.Lens as I++import qualified Data.Fin      as F+import qualified Data.Type.Nat as N+import qualified Data.Vec.Pull as P++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Convert to pull 'P.Vec'.+toPull :: forall n a. N.InlineInduction n => Vec n a -> P.Vec n a+toPull = getToPull (N.inlineInduction1 start step) where+    start :: ToPull 'Z a+    start = ToPull $ \_ -> P.Vec F.absurd++    step :: ToPull m a -> ToPull ('S m) a+    step (ToPull f) = ToPull $ \(x ::: xs) -> P.Vec $ \i -> case i of+        F.Z    -> x+        F.S i' -> P.unVec (f xs) i'++newtype ToPull n a = ToPull { getToPull :: Vec n a -> P.Vec n a }++-- | Convert from pull 'P.Vec'.+fromPull :: forall n a. N.InlineInduction n => P.Vec n a -> Vec n a+fromPull = getFromPull (N.inlineInduction1 start step) where+    start :: FromPull 'Z a+    start = FromPull $ const VNil++    step :: FromPull m a -> FromPull ('S m) a+    step (FromPull f) = FromPull $ \(P.Vec v) -> v F.Z ::: f (P.Vec (v . F.S))++newtype FromPull n a = FromPull { getFromPull :: P.Vec n a -> Vec n a }++-- | An 'I.Iso' from 'toPull' and 'fromPull'.+_Pull :: N.InlineInduction n => I.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)+_Pull = I.iso toPull fromPull++-- | Convert 'Vec' to list.+--+-- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil+-- "foo"+toList :: forall n a. N.InlineInduction n => Vec n a -> [a]+toList = getToList (N.inlineInduction1 start step) where+    start :: ToList 'Z a+    start = ToList (const [])++    step :: ToList m a -> ToList ('S m) a+    step (ToList f) = ToList $ \(x ::: xs) -> x : f xs++newtype ToList n a = ToList { getToList :: Vec n a -> [a] }++-- | Convert list @[a]@ to @'Vec' n a@.+-- Returns 'Nothing' if lengths don't match exactly.+--+-- >>> fromList "foo" :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> fromList "quux" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+-- >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+fromList :: N.InlineInduction n => [a] -> Maybe (Vec n a)+fromList = getFromList (N.inlineInduction1 start step) where+    start :: FromList 'Z a+    start = FromList $ \xs -> case xs of+        []      -> Just VNil+        (_ : _) -> Nothing++    step :: FromList n a -> FromList ('N.S n) a+    step (FromList f) = FromList $ \xs -> case xs of+        []       -> Nothing+        (x : xs') -> (x :::) <$> f xs'++newtype FromList n a = FromList { getFromList :: [a] -> Maybe (Vec n a) }++-- | Prism from list.+--+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)+-- Nothing+--+-- >>> _Vec # (True ::: False ::: VNil)+-- [True,False]+--+_Vec :: N.InlineInduction n => I.Prism' [a] (Vec n a)+_Vec = I.prism' toList fromList++-- | Convert list @[a]@ to @'Vec' n a@.+-- Returns 'Nothing' if input list is too short.+--+-- >>> fromListPrefix "foo" :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> fromListPrefix "quux" :: Maybe (Vec N.Nat3 Char)+-- Just ('q' ::: 'u' ::: 'u' ::: VNil)+--+-- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+fromListPrefix :: N.InlineInduction n => [a] -> Maybe (Vec n a)+fromListPrefix = getFromList (N.inlineInduction1 start step) where+    start :: FromList 'Z a+    start = FromList $ \_ -> Just VNil -- different than in fromList case++    step :: FromList n a -> FromList ('N.S n) a+    step (FromList f) = FromList $ \xs -> case xs of+        []       -> Nothing+        (x : xs') -> (x :::) <$> f xs'++-------------------------------------------------------------------------------+-- Indexing+-------------------------------------------------------------------------------++-- | Indexing.+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! F.S F.Z+-- 'b'+--+(!) :: N.InlineInduction n => Vec n a -> Fin n -> a+(!) = appIndex (N.inlineInduction1 start step) where+    start :: Index 'Z a+    start = Index $ \_ -> F.absurd++    step :: Index n a -> Index ('S n) a+    step (Index f) = Index $ \xs i -> case xs of+        x ::: xs' -> case i of+            F.Z    -> x+            F.S i' -> f xs' i'++newtype Index n a = Index { appIndex :: Vec n a -> Fin n -> a }++-- | Index lens.+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)+-- 'b'+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ 'x'+-- 'a' ::: 'x' ::: 'c' ::: VNil+--+ix :: N.InlineInduction n => Fin n -> I.Lens' (Vec n a) a+ix = getIxLens $ N.inlineInduction1 start step where+    start :: IxLens 'Z a+    start = IxLens F.absurd++    step :: IxLens m a -> IxLens ('S m) a+    step (IxLens l) = IxLens $ \i -> case i of+        F.Z   -> _head+        F.S j -> _tail . l j++newtype IxLens n a = IxLens { getIxLens :: Fin n -> I.Lens' (Vec n a) a }++-------------------------------------------------------------------------------+-- Concatenation+-------------------------------------------------------------------------------++infixr 5 ++++-- | Append two 'Vec'.+--+-- >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)+-- 'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil+--+(++) :: forall n m a. N.InlineInduction n => Vec n a -> Vec m a -> Vec (N.Plus n m) a+as ++ ys = getAppend (N.inlineInduction1 start step) as where+    start :: Append m 'Z a+    start = Append $ \_ -> ys++    step :: Append m p a -> Append m ('S p) a+    step (Append f) = Append $ \(x ::: xs) -> x ::: f xs++newtype Append m n a = Append { getAppend :: Vec n a -> Vec (N.Plus n m) a }++-- | Split vector into two parts. Inverse of '++'.+--+-- >>> split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)+-- ('a' ::: VNil,'b' ::: 'c' ::: VNil)+--+-- >>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))+-- 'a' ::: 'b' ::: 'c' ::: VNil+--+split :: N.InlineInduction n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)+split = appSplit (N.inlineInduction1 start step) where+    start :: Split m 'Z a+    start = Split $ \xs -> (VNil, xs)++    step :: Split m n a -> Split m ('S n) a+    step (Split f) = Split $ \(x ::: xs) -> case f xs of+        (ys, zs) -> (x ::: ys, zs)++newtype Split m n a = Split { appSplit :: Vec (N.Plus n m) a -> (Vec n a, Vec m a) }+-- | Map over all the elements of a 'Vec' and concatenate the resulting 'Vec's.+--+-- >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)+-- 'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil+--+concatMap :: forall a b n m. (N.InlineInduction m, N.InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b+concatMap f = getConcatMap $ N.inlineInduction1 start step where+    start :: ConcatMap m a 'Z b+    start = ConcatMap $ \_ -> VNil++    step :: ConcatMap m a p b -> ConcatMap m a ('S p) b+    step (ConcatMap g) = ConcatMap $ \(x ::: xs) -> f x ++ g xs++newtype ConcatMap m a n b = ConcatMap { getConcatMap :: Vec n a -> Vec (N.Mult n m) b }++-- | @'concatMap' 'id'@+concat :: (N.InlineInduction m, N.InlineInduction n) => Vec n (Vec m a) -> Vec (N.Mult n m) a+concat = concatMap id++-- | Inverse of 'concat'.+--+-- >>> chunks <$> fromListPrefix [1..] :: Maybe (Vec N.Nat2 (Vec N.Nat3 Int))+-- Just ((1 ::: 2 ::: 3 ::: VNil) ::: (4 ::: 5 ::: 6 ::: VNil) ::: VNil)+--+-- >>> let idVec x = x :: Vec N.Nat2 (Vec N.Nat3 Int)+-- >>> concat . idVec . chunks <$> fromListPrefix [1..]+-- Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)+--+chunks :: (N.InlineInduction n, N.InlineInduction m) => Vec (N.Mult n m) a -> Vec n (Vec m a)+chunks = getChunks $ N.induction1 start step where+    start :: Chunks m 'Z a+    start = Chunks $ \_ -> VNil++    step :: forall m n a. N.InlineInduction m => Chunks m n a -> Chunks m ('S n) a+    step (Chunks go) = Chunks $ \xs ->+        let (ys, zs) = split xs :: (Vec m a, Vec (N.Mult n m) a)+        in ys ::: go zs++newtype Chunks  m n a = Chunks  { getChunks  :: Vec (N.Mult n m) a -> Vec n (Vec m a) }++-------------------------------------------------------------------------------+-- Mapping+-------------------------------------------------------------------------------++-- | >>> map not $ True ::: False ::: VNil+-- False ::: True ::: VNil+--+map :: forall a b n. N.InlineInduction n => (a -> b) -> Vec n a -> Vec n b+map f = getMap $ N.inlineInduction1 start step where+    start :: Map a 'Z b+    start = Map $ \_ -> VNil++    step :: Map a m b -> Map a ('S m) b+    step (Map go) = Map $ \(x ::: xs) -> f x ::: go xs++newtype Map a n b = Map { getMap :: Vec n a -> Vec n b }++-- | >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil+-- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil+--+imap :: N.InlineInduction n => (Fin n -> a -> b) -> Vec n a -> Vec n b+imap = getIMap $ N.inlineInduction1 start step where+    start :: IMap a 'Z b+    start = IMap $ \_ _ -> VNil++    step :: IMap a m b -> IMap a ('S m) b+    step (IMap go) = IMap $ \f (x ::: xs) -> f F.Z x ::: go (f . F.S) xs++newtype IMap a n b = IMap { getIMap :: (Fin n -> a -> b) -> Vec n a -> Vec n b }++-- | Apply an action to every element of a 'Vec', yielding a 'Vec' of results.+traverse :: forall n f a b. (Applicative f, N.InlineInduction n) => (a -> f b) -> Vec n a -> f (Vec n b)+traverse f =  getTraverse $ N.inlineInduction1 start step where+    start :: Traverse f a 'Z b+    start = Traverse $ \_ -> pure VNil++    step :: Traverse f a m b -> Traverse f a ('S m) b+    step (Traverse go) = Traverse $ \(x ::: xs) -> liftA2 (:::) (f x) (go xs)++newtype Traverse f a n b = Traverse { getTraverse :: Vec n a -> f (Vec n b) }++-- | Apply an action to non-empty 'Vec', yielding a 'Vec' of results.+traverse1 :: forall n f a b. (Apply f, N.InlineInduction n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)+traverse1 f = getTraverse1 $ N.inlineInduction1 start step where+    start :: Traverse1 f a 'Z b+    start = Traverse1 $ \(x ::: _) -> (::: VNil) <$> f x++    step :: Traverse1 f a m b -> Traverse1 f a ('S m) b+    step (Traverse1 go) = Traverse1 $ \(x ::: xs) -> liftF2 (:::) (f x) (go xs)++newtype Traverse1 f a n b = Traverse1 { getTraverse1 :: Vec ('S n) a -> f (Vec ('S n) b) }++-- | Apply an action to every element of a 'Vec' and its index, yielding a 'Vec' of results.+itraverse :: forall n f a b. (Applicative f, N.InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)+itraverse = getITraverse $ N.inlineInduction1 start step where+    start :: ITraverse f a 'Z b+    start = ITraverse $ \_ _ -> pure VNil++    step :: ITraverse f a m b -> ITraverse f a ('S m) b+    step (ITraverse go) = ITraverse $ \f (x ::: xs) -> liftA2 (:::) (f F.Z x) (go (f . F.S) xs)++newtype ITraverse f a n b = ITraverse { getITraverse :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) }++-- | Apply an action to every element of a 'Vec' and its index, ignoring the results.+itraverse_ :: forall n f a b. (Applicative f, N.InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f ()+itraverse_ = getITraverse_ $ N.inlineInduction1 start step where+    start :: ITraverse_ f a 'Z b+    start = ITraverse_ $ \_ _ -> pure ()++    step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b+    step (ITraverse_ go) = ITraverse_ $ \f (x ::: xs) -> f F.Z x *> go (f . F.S) xs++newtype ITraverse_ f a n b = ITraverse_ { getITraverse_ :: (Fin n -> a -> f b) -> Vec n a -> f () }++-------------------------------------------------------------------------------+-- Folding+-------------------------------------------------------------------------------++-- | See 'I.Foldable'.+foldMap :: (Monoid m, N.InlineInduction n) => (a -> m) -> Vec n a -> m+foldMap f = getFold $ N.inlineInduction1 (Fold (const mempty)) $ \(Fold go) ->+    Fold $ \(x ::: xs) -> f x `mappend` go xs++newtype Fold  a n b = Fold  { getFold  :: Vec n a -> b }++-- | See 'I.Foldable1'.+foldMap1 :: forall s a n. (Semigroup s, N.InlineInduction n) => (a -> s) -> Vec ('S n) a -> s+foldMap1 f = getFold1 $ N.inlineInduction1 start step where+    start :: Fold1 a 'Z s+    start = Fold1 $ \(x ::: _) -> f x++    step :: Fold1 a m s -> Fold1 a ('S m) s+    step (Fold1 g) = Fold1 $ \(x ::: xs) -> f x <> g xs++newtype Fold1 a n b = Fold1 { getFold1 :: Vec ('S n) a -> b }++-- | See 'I.FoldableWithIndex'.+ifoldMap :: forall a n m. (Monoid m, N.InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m+ifoldMap = getIFoldMap $ N.inlineInduction1 start step where+    start :: IFoldMap a 'Z m+    start = IFoldMap $ \_ _ -> mempty++    step :: IFoldMap a p m -> IFoldMap a ('S p) m+    step (IFoldMap go) = IFoldMap $ \f (x ::: xs) -> f F.Z x `mappend` go (f . F.S) xs++newtype IFoldMap a n m = IFoldMap { getIFoldMap :: (Fin n -> a -> m) -> Vec n a -> m }++-- | There is no type-class for this :(+ifoldMap1 :: forall a n s. (Semigroup s, N.InlineInduction n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s+ifoldMap1 = getIFoldMap1 $ N.inlineInduction1 start step where+    start :: IFoldMap1 a 'Z s+    start = IFoldMap1 $ \f (x ::: _) -> f F.Z x++    step :: IFoldMap1 a p s -> IFoldMap1 a ('S p) s+    step (IFoldMap1 go) = IFoldMap1 $ \f (x ::: xs) -> f F.Z x <> go (f . F.S) xs++newtype IFoldMap1 a n m = IFoldMap1 { getIFoldMap1 :: (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m }++-- | Right fold.+foldr :: forall a b n. N.InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b+foldr f z = getFold $ N.inlineInduction1 start step where+    start :: Fold a 'Z b+    start = Fold $ \_ -> z++    step :: Fold a m b -> Fold a ('S m) b+    step (Fold go) = Fold $ \(x ::: xs) -> f x (go xs)++-- | Right fold with an index.+ifoldr :: forall a b n. N.InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b+ifoldr = getIFoldr $ N.inlineInduction1 start step where+    start :: IFoldr a 'Z b+    start = IFoldr $ \_ z _ -> z++    step :: IFoldr a m b -> IFoldr a ('S m) b+    step (IFoldr go) = IFoldr $ \f z (x ::: xs) -> f F.Z x (go (f . F.S) z xs)++newtype IFoldr a n b = IFoldr { getIFoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b }++-- | Yield the length of a 'Vec'. /O(n)/+length :: forall n a. N.InlineInduction n => Vec n a -> Int+length _ = getLength l where+    l :: Length n+    l = N.inlineInduction (Length 0) $ \(Length n) -> Length (1 + n)++newtype Length (n :: Nat) = Length { getLength :: Int }++-------------------------------------------------------------------------------+-- Special folds+-------------------------------------------------------------------------------++-- | Non-strict 'sum'.+sum :: (Num a, N.InlineInduction n) => Vec n a -> a+sum = getFold $ N.inlineInduction1 start step where+    start :: Num a => Fold a 'Z a+    start = Fold $ \_ -> 0++    step :: Num a => Fold a m a -> Fold a ('S m) a+    step (Fold f) = Fold $ \(x ::: xs) -> x + f xs++-- | Non-strict 'product'.+product :: (Num a, N.InlineInduction n) => Vec n a -> a+product = getFold $ N.inlineInduction1 start step where+    start :: Num a => Fold a 'Z a+    start = Fold $ \_ -> 0++    step :: Num a => Fold a m a -> Fold a ('S m) a+    step (Fold f) = Fold $ \(x ::: xs) -> x + f xs++-------------------------------------------------------------------------------+-- Zipping+-------------------------------------------------------------------------------++-- | Zip two 'Vec's with a function.+zipWith :: forall a b c n. N.InlineInduction n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+zipWith f = getZipWith $ N.inlineInduction start step where+    start :: ZipWith a b c 'Z+    start = ZipWith $ \_ _ -> VNil++    step :: ZipWith a b c m -> ZipWith a b c ('S m)+    step (ZipWith go) = ZipWith $ \(x ::: xs) (y ::: ys) -> f x y ::: go xs ys++newtype ZipWith a b c n = ZipWith { getZipWith :: Vec n a -> Vec n b -> Vec n c }++-- | Zip two 'Vec's. with a function that also takes the elements' indices.+izipWith :: N.InlineInduction n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+izipWith = getIZipWith $ N.inlineInduction start step where+    start :: IZipWith a b c 'Z+    start = IZipWith $ \_ _ _ -> VNil++    step :: IZipWith a b c m -> IZipWith a b c ('S m)+    step (IZipWith go) = IZipWith $ \f (x ::: xs) (y ::: ys) -> f F.Z x y ::: go (f . F.S) xs ys++newtype IZipWith a b c n = IZipWith { getIZipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c }++-------------------------------------------------------------------------------+-- Monadic+-------------------------------------------------------------------------------++-- | Monadic bind.+bind :: N.InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b+bind = getBind $ N.inlineInduction1 start step where+    start :: Bind a 'Z b+    start = Bind $ \_ _ -> VNil++    step :: Bind a m b -> Bind a ('S m) b+    step (Bind go) = Bind $ \(x ::: xs) f -> head (f x) ::: go xs (tail . f)++newtype Bind a n b = Bind { getBind :: Vec n a -> (a -> Vec n b) -> Vec n b }++-- | Monadic join.+--+-- >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil+-- 'a' ::: 'd' ::: VNil+join :: N.InlineInduction n => Vec n (Vec n a) -> Vec n a+join = getJoin $ N.inlineInduction1 start step where+    start :: Join 'Z a+    start = Join $ \_ -> VNil++    step :: N.InlineInduction m => Join m a -> Join ('S m) a+    step (Join go) = Join $ \(x ::: xs) -> head x ::: go (map tail xs)++newtype Join n a = Join { getJoin :: Vec n (Vec n a) -> Vec n a }++-------------------------------------------------------------------------------+-- universe+-------------------------------------------------------------------------------++-- | Get all @'Fin' n@ in a @'Vec' n@.+--+-- >>> universe :: Vec N.Nat3 (Fin N.Nat3)+-- 0 ::: 1 ::: 2 ::: VNil+universe :: N.InlineInduction n => Vec n (Fin n)+universe = getUniverse (N.inlineInduction first step) where+    first :: Universe 'Z+    first = Universe VNil++    step :: N.InlineInduction m => Universe m -> Universe ('S m)+    step (Universe go) = Universe (F.Z ::: map F.S go)++newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }++-------------------------------------------------------------------------------+-- Doctest+-------------------------------------------------------------------------------++-- $setup+-- >>> :set -XScopedTypeVariables+-- >>> import Control.Lens ((^.), (&), (.~), (^?), (#))+-- >>> import Data.Proxy (Proxy (..))+-- >>> import Prelude.Compat (Char, Bool (..), not, uncurry)
+ src/Data/Vec/Pull.hs view
@@ -0,0 +1,409 @@+{-# LANGUAGE CPP                   #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+-- | Pull/representable @'Vec' n a = 'Fin' n -> a@.+--+-- The module tries to have same API as "Data.Vec.Lazy", missing bits:+-- @withDict@, @toPull@, @fromPull@, @traverse@ (and variants),+-- @(++)@, @concat@ and @split@.+module Data.Vec.Pull (+    Vec (..),+    -- * Construction+    empty,+    singleton,+    -- * Conversions+    toList,+    fromList,+    _Vec,+    fromListPrefix,+    reifyList,+    -- * Indexing+    (!),+    ix,+    _Cons,+    _head,+    _tail,+    head,+    tail,+    -- * Folds+    foldMap,+    foldMap1,+    ifoldMap,+    ifoldMap1,+    foldr,+    ifoldr,+    foldl',+    -- * Special folds+    length,+    null,+    sum,+    product,+    -- * Mapping+    map,+    imap,+    -- * Zipping+    zipWith,+    izipWith,+    -- * Monadic+    bind,+    join,+    -- * Universe+    universe,+    ) where++import Prelude ()+import Prelude.Compat+       (Bool (..), Eq (..), Functor (..), Int, Maybe (..),+       Monad (..), Monoid (..), Num (..), all, const, id, ($), (.), (<$>))++import Control.Applicative (Applicative (..))+import Control.Lens        ((<&>))+import Data.Boring         (Boring (..))+import Data.Distributive   (Distributive (..))+import Data.Fin            (Fin)+import Data.Functor.Apply  (Apply (..))+import Data.Functor.Rep    (Representable (..))+import Data.Nat+import Data.Proxy          (Proxy (..))+import Data.Semigroup      (Semigroup (..))+import Data.Typeable       (Typeable)++--- Instances+import qualified Control.Lens            as I+import qualified Data.Foldable           as I (Foldable (..))+import qualified Data.Functor.Bind       as I (Bind (..))+import qualified Data.Semigroup.Foldable as I (Foldable1 (..))++import qualified Data.Fin      as F+import qualified Data.Type.Nat as N++-- | Easily fuseable 'Vec'.+--+-- It unpurpose don't have /bad/ (fusion-wise) instances, like 'Traversable'.+-- Generally, there aren't functions which would be __bad consumers__ or __bad producers__.+newtype Vec n a = Vec { unVec :: Fin n -> a }+  deriving (Typeable)++instance (Eq a, N.SNatI n) => Eq (Vec n a) where+    Vec v == Vec u = all (\i -> u i == v i) F.universe++instance Functor (Vec n) where+    fmap f (Vec v) = Vec (f . v)++instance N.SNatI n => I.Foldable (Vec n) where+    foldMap = foldMap++instance Applicative (Vec n) where+    pure   = Vec . pure+    (<*>)  = zipWith ($)+    _ *> x = x+    x <* _ = x+#if MIN_VERSION_base(4,10,0)+    liftA2 = zipWith+#endif++instance Monad (Vec n) where+    return = pure+    (>>=)  = bind+    _ >> x = x++instance Distributive (Vec n) where+    distribute = Vec . distribute . fmap unVec++instance Representable (Vec n) where+    type Rep (Vec n) = Fin n+    tabulate = Vec+    index    = unVec++instance Semigroup a => Semigroup (Vec n a) where+    Vec a <> Vec b = Vec (a <> b)++instance Monoid a => Monoid (Vec n a) where+    mempty = Vec mempty+    Vec a `mappend` Vec b = Vec (mappend a b)++instance n ~ 'N.Z => Boring (Vec n a) where+    boring = empty++instance Apply (Vec n) where+    (<.>)  = zipWith ($)+    _ .> x = x+    x <. _ = x++instance I.Bind (Vec n) where+    (>>-) = bind+    join  = join++instance I.FunctorWithIndex (Fin n) (Vec n) where+    imap = imap++instance N.SNatI n => I.FoldableWithIndex (Fin n) (Vec n) where+    ifoldMap = ifoldMap+    ifoldr   = ifoldr++-------------------------------------------------------------------------------+-- Construction+-------------------------------------------------------------------------------++-- | Empty 'Vec'.+empty :: Vec 'Z a+empty = Vec F.absurd++-- | 'Vec' with exactly one element.+--+-- >>> L.fromPull $ singleton True+-- True ::: VNil+--+singleton :: a -> Vec ('S 'Z) a+singleton = Vec . const++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Convert 'Vec' to list.+toList :: N.SNatI n => Vec n a -> [a]+toList v = unVec v <$> F.universe++-- | Convert list @[a]@ to @'Vec' n a@.+-- Returns 'Nothing' if lengths don't match exactly.+--+-- >>> L.fromPull <$> fromList "foo" :: Maybe (L.Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> L.fromPull <$> fromList "quux" :: Maybe (L.Vec N.Nat3 Char)+-- Nothing+--+-- >>> L.fromPull <$> fromList "xy" :: Maybe (L.Vec N.Nat3 Char)+-- Nothing+--+fromList :: N.SNatI n => [a] -> Maybe (Vec n a)+fromList = getFromList (N.induction1 start step) where+    start :: FromList 'Z a+    start = FromList $ \xs -> case xs of+        []      -> Just empty+        (_ : _) -> Nothing++    step :: FromList n a -> FromList ('N.S n) a+    step (FromList f) = FromList $ \xs -> case xs of+        []        -> Nothing+        (x : xs') -> cons x <$> f xs'++newtype FromList n a = FromList { getFromList :: [a] -> Maybe (Vec n a) }++-- | Prism from list.+_Vec :: N.SNatI n => I.Prism' [a] (Vec n a)+_Vec = I.prism' toList fromList++-- | Convert list @[a]@ to @'Vec' n a@.+-- Returns 'Nothing' if input list is too short.+--+-- >>> L.fromPull <$> fromListPrefix "foo" :: Maybe (L.Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> L.fromPull <$> fromListPrefix "quux" :: Maybe (L.Vec N.Nat3 Char)+-- Just ('q' ::: 'u' ::: 'u' ::: VNil)+--+-- >>> L.fromPull <$> fromListPrefix "xy" :: Maybe (L.Vec N.Nat3 Char)+-- Nothing+--+fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)+fromListPrefix = getFromList (N.induction1 start step) where+    start :: FromList 'Z a+    start = FromList $ \_ -> Just empty -- different than in fromList case++    step :: FromList n a -> FromList ('N.S n) a+    step (FromList f) = FromList $ \xs -> case xs of+        []       -> Nothing+        (x : xs') -> cons x <$> f xs'++-- | Reify any list @[a]@ to @'Vec' n a@.+--+-- >>> reifyList "foo" length+-- 3+reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r+reifyList []       f = f empty+reifyList (x : xs) f = reifyList xs $ \xs' -> f (cons x xs')++-------------------------------------------------------------------------------+-- Indexing+-------------------------------------------------------------------------------++-- | Indexing.+(!) :: Vec n a -> Fin n -> a+(!) = unVec++-- | Index lens.+--+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . ix (F.S F.Z)+-- 'b'+--+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . ix (F.S F.Z) .~ 'x'+-- 'a' ::: 'x' ::: 'c' ::: VNil+--+ix :: Fin n -> I.Lens' (Vec n a) a+ix i f (Vec v) = f (v i) <&> \a -> Vec $ \j ->+    if i == j+    then a+    else v j++-- | Match on non-empty 'Vec'.+--+-- /Note:/ @lens@ 'I._Cons' is a 'I.Prism'.+-- In fact, @'Vec' n a@ cannot have an instance of 'I.Cons' as types don't match.+--+_Cons :: I.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)+_Cons = I.iso (\(Vec v) -> (v F.Z, Vec (v . F.S))) (\(x, xs) -> cons x xs)++-- | Head lens. /Note:/ @lens@ 'I._head' is a 'I.Traversal''.+--+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . _head+-- 'a'+--+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . _head .~ 'x'+-- 'x' ::: 'b' ::: 'c' ::: VNil+--+_head :: I.Lens' (Vec ('S n) a) a+_head f (Vec v) = f (v F.Z) <&> \a -> Vec $ \j -> case j of+    F.Z -> a+    _   -> v j+{-# INLINE head #-}++-- | Head lens. /Note:/ @lens@ 'I._head' is a 'I.Traversal''.+_tail :: I.Lens' (Vec ('S n) a) (Vec n a)+_tail f (Vec v) = f (Vec (v . F.S)) <&> \xs -> cons (v F.Z) xs+{-# INLINE _tail #-}++cons :: a -> Vec n a -> Vec ('S n) a+cons x (Vec v) = Vec $ \i -> case i of+    F.Z   -> x+    F.S j -> v j++-- | The first element of a 'Vec'.+head :: Vec ('S n) a -> a+head (Vec v) = v F.Z++-- | The elements after the 'head' of a 'Vec'.+tail :: Vec ('S n) a -> Vec n a+tail (Vec v) = Vec (v . F.S)++-------------------------------------------------------------------------------+-- Mapping+-------------------------------------------------------------------------------++-- | >>> over L._Pull (map not) (True L.::: False L.::: L.VNil)+-- False ::: True ::: VNil+--+map :: (a -> b) -> Vec n a -> Vec n b+map f (Vec v) = Vec (f . v)++-- | >>> over L._Pull (imap (,)) ('a' L.::: 'b' L.::: 'c' L.::: L.VNil)+-- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil+--+imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b+imap f (Vec v) = Vec $ \i -> f i (v i)++-------------------------------------------------------------------------------+-- Folding+-------------------------------------------------------------------------------++-- | See 'I.Foldable'.+foldMap :: (Monoid m, N.SNatI n) => (a -> m) -> Vec n a -> m+foldMap f (Vec v) = I.foldMap (f . v) F.universe++-- | See 'I.Foldable1'.+foldMap1 :: (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s+foldMap1 f (Vec v) = I.foldMap1 (f . v) F.universe1++-- | See 'I.FoldableWithIndex'.+ifoldMap :: (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m+ifoldMap f (Vec v) = I.foldMap (\i -> f i (v i)) F.universe++-- | There is no type-class for this :(+ifoldMap1 :: (Semigroup s, N.SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s+ifoldMap1 f (Vec v) = I.foldMap1 (\i -> f i (v i)) F.universe1++-- | Right fold.+foldr :: N.SNatI n => (a -> b -> b) -> b -> Vec n a -> b+foldr f z (Vec v) = I.foldr (\a b -> f (v a) b) z F.universe++-- | Right fold with an index.+ifoldr :: N.SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b+ifoldr f z (Vec v) = I.foldr (\a b -> f a (v a) b) z F.universe++-- | Strict left fold.+foldl' :: N.SNatI n => (b -> a -> b) -> b -> Vec n a -> b+foldl' f z (Vec v) = I.foldl' (\b a -> f b (v a)) z F.universe++-- | Yield the length of a 'Vec'.+length :: forall n a. N.SNatI n => Vec n a -> Int+length _ = N.reflectToNum (Proxy :: Proxy n)++-- | Test whether a 'Vec' is empty.+null :: forall n a. N.SNatI n => Vec n a -> Bool+null _ = case N.snat :: N.SNat n of+    N.SZ -> True+    N.SS -> False++-------------------------------------------------------------------------------+-- Special folds+-------------------------------------------------------------------------------++-- | Strict 'sum'.+sum :: (Num a, N.SNatI n) => Vec n a -> a+sum (Vec v) = I.foldl' (\x i -> x + v i) 0 F.universe++-- | Strict 'product'.+product :: (Num a, N.SNatI n) => Vec n a -> a+product (Vec v) = I.foldl' (\x i -> x * v i) 1 F.universe++-------------------------------------------------------------------------------+-- Zipping+-------------------------------------------------------------------------------++-- | Zip two 'Vec's with a function.+zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+zipWith f (Vec xs) (Vec ys) = Vec $ \i -> f (xs i) (ys i)++-- | Zip two 'Vec's. with a function that also takes the elements' indices.+izipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+izipWith f (Vec xs) (Vec ys) = Vec $ \i -> f i (xs i) (ys i)++-------------------------------------------------------------------------------+-- Monadic+-------------------------------------------------------------------------------++-- | Monadic bind.+bind :: Vec n a -> (a -> Vec n b) -> Vec n b+bind m k = Vec $ unVec m >>= unVec . k++-- | Monadic join.+join :: Vec n (Vec n a) -> Vec n a+join (Vec v) = Vec $ \i -> unVec (v i) i++-------------------------------------------------------------------------------+-- Universe+-------------------------------------------------------------------------------++-- | Get all @'Fin' n@ in a @'Vec' n@.+--+-- >>> L.fromPull (universe :: Vec N.Nat3 (Fin N.Nat3))+-- 0 ::: 1 ::: 2 ::: VNil+universe :: N.SNatI n => Vec n (Fin n)+universe = Vec id++-------------------------------------------------------------------------------+-- Doctest+-------------------------------------------------------------------------------++-- $setup+-- >>> :set -XScopedTypeVariables+-- >>> import Control.Lens ((^.), (&), (.~), over)+-- >>> import Data.Proxy (Proxy (..))+-- >>> import Prelude.Compat (Char, Bool (..), not)+-- >>> import qualified Data.Vec.Lazy as L
+ test/Inspection.hs view
@@ -0,0 +1,95 @@+{-# LANGUAGE GADTs           #-}+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}+module Main (main) where++import Prelude hiding (zipWith)++import Data.Vec.Lazy   (Vec (..))+import Test.Inspection++import qualified Data.Fin             as F+import qualified Data.Type.Nat        as N+import qualified Data.Vec.Lazy        as L+import qualified Data.Vec.Lazy.Inline as I++-------------------------------------------------------------------------------+-- zipWith+-------------------------------------------------------------------------------++-- | This doesn't evaluate compile time.+lhsInline :: Vec N.Nat2 Int+lhsInline = I.zipWith (+) xs ys++-- | This doesn't evaluate compile time.+lhsNormal :: Vec N.Nat2 Int+lhsNormal = L.zipWith (+) xs ys++xs :: Vec N.Nat2 Int+xs = 1 ::: 2 ::: VNil++ys :: Vec N.Nat2 Int+ys = 2 ::: 3 ::: VNil++rhsZipWith :: Vec N.Nat2 Int+rhsZipWith = 3 ::: 5 ::: VNil++inspect $ 'lhsInline === 'rhsZipWith+inspect $ 'lhsNormal =/= 'rhsZipWith++-------------------------------------------------------------------------------+-- imap+-------------------------------------------------------------------------------++lhsIMap :: Vec N.Nat2 (F.Fin N.Nat2, Char)+lhsIMap = I.imap (,) $ 'a' ::: 'b' ::: VNil++lhsIMap' :: Vec N.Nat2 (F.Fin N.Nat2, Char)+lhsIMap' = L.imap (,) $ 'a' ::: 'b' ::: VNil++rhsIMap :: Vec N.Nat2 (F.Fin N.Nat2, Char)+rhsIMap = (F.Z,'a') ::: (F.S F.Z,'b') ::: VNil++inspect $ 'lhsIMap  === 'rhsIMap+inspect $ 'lhsIMap' =/= 'rhsIMap++-------------------------------------------------------------------------------+-- dotProduct+-------------------------------------------------------------------------------++{-+ -- TODO: for this example LHS produces better core :O+ -- though, inlining isn't done if element is Num a => a+ --+lhsDotProduct :: Vec N.Nat2 Int -> Vec N.Nat2 Int -> Int+lhsDotProduct xs ys = I.sum (I.zipWith (+) xs ys)++rhsDotProduct :: Vec N.Nat2 Int -> Vec N.Nat2 Int -> Int+rhsDotProduct (x0 ::: x1 ::: _) (y0 ::: y1 ::: _) =+    x0 * y0 + x1 * y1++inspect $ 'lhsDotProduct === 'rhsDotProduct+-}++-------------------------------------------------------------------------------+-- join+-------------------------------------------------------------------------------++lhsJoin :: Vec N.Nat2 Char+lhsJoin = I.join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil++lhsJoin' :: Vec N.Nat2 Char+lhsJoin' = L.join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil++rhsJoin :: Vec N.Nat2 Char+rhsJoin = 'a' ::: 'd' ::: VNil++inspect $ 'lhsJoin  === 'rhsJoin+inspect $ 'lhsJoin' =/= 'rhsJoin++-------------------------------------------------------------------------------+-- Main to make GHC happy+-------------------------------------------------------------------------------++main :: IO ()+main = return ()
+ vec.cabal view
@@ -0,0 +1,130 @@+name:                vec+version:             0+synopsis:            Nat, Fin and Vec types.+description:+  This package provides length indexed lists, i.e. 'Vec'.+  .+  @+  data Vec n a where+      VNil  :: Vec 'Nat.Z a+      (:::) :: a -> Vec n a -> Vec ('Nat.S n) a+  @+  .+  The functions are implemented in three flavours:+  .+  * __naive__: with explicit recursion. It's simple, constraint-less, yet slow.+  .+  * __pull__: using @Fin n -> a@ representation, which fuses well,+    but makes some programs hard to write. And+  .+  * __inline__: which exploits how GHC dictionary inlining works, unrolling+    recursion if the size of 'Vec' is known statically.+  .+  As best approach depends on the application, @vec@ doesn't do any magic+  transformation. Benchmark your code.+  .+  Differences to other packages:+  .+  * [linear](http://hackage.haskell.org/package/linear) has 'V' type,+    which uses 'Vector' from @vector@ package as backing store.+    `Vec` is a real GADT, but tries to provide as many useful instances (upto @lens@).+  .+  * [sized-vector](http://hackage.haskell.org/package/sized-vector) depends+    on @singletons@ package. `vec` isn't light on dependencies either,+    but try to provide wide GHC support.+  .+  * [sized](https://hackage.haskell.org/package/sized) also depends+    on a @singletons@ package. The @Sized f n a@ type is generalisation of+    @linear@'s @V@ for any @ListLike@.+  .+  * [clash-prelude](https://hackage.haskell.org/package/clash-prelude)+    is a kitchen sink package, which has @CLaSH.Sized.Vector@ module.+    Also depends on @singletons@.++homepage:            https://github.com/phadej/vec+bug-reports:         https://github.com/phadej/vec/issues+license:             BSD3+license-file:        LICENSE+author:              Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:          Oleg.Grenrus <oleg.grenrus@iki.fi>+copyright:           (c) 2017 Oleg Grenrus+category:            Data+build-type:          Simple+extra-source-files:  ChangeLog.md+cabal-version:       >=1.10+tested-with:+  GHC==7.8.4,+  GHC==7.10.3,+  GHC==8.0.2,+  GHC==8.2.1++source-repository head+  type:      git+  location:  https://github.com/phadej/vec.git++library+  exposed-modules:+    Data.Vec.Lazy+    Data.Vec.Lazy.Inline+    Data.Vec.Pull+  build-depends:+    adjunctions   >=4.3     && <4.4,+    base          >=4.7     && <4.11,+    base-compat   >=0.9.3   && <0.10,+    boring        >=0       && <0.1,+    deepseq       >=1.3.0.2 && <1.5,+    distributive  >=0.5.3   && <0.6,+    fin           >=0       && <0.1,+    hashable      >=1.2.6.1 && <1.3,+    lens          >=4.15.4  && <4.16,+    semigroupoids >=5.2.1   && <5.3,+    semigroups    >=0.18.3  && <0.18.4++  ghc-options:         -Wall -fprint-explicit-kinds+  hs-source-dirs:      src+  other-extensions:+    CPP+    FlexibleContexts+    GADTs+    TypeOperators+  default-language:    Haskell2010++test-suite inspection+  type:                exitcode-stdio-1.0+  main-is:             Inspection.hs+  ghc-options:         -Wall -fprint-explicit-kinds+  hs-source-dirs:      test+  default-language:    Haskell2010+  build-depends:+    base,+    fin,+    vec,+    tagged,+    inspection-testing >= 0.1.1.2 && <0.2++  if !impl(ghc >= 8.0)+    buildable: False++  -- useful for development+  ghc-options:+    -- -dsuppress-idinfo+    -- -dsuppress-coercions+    -- -dsuppress-type-applications+    -- -dsuppress-module-prefixes+    -- -dsuppress-type-signatures+    -- -dsuppress-uniques++benchmark bench+  type:                exitcode-stdio-1.0+  main-is:             Bench.hs+  ghc-options:         -Wall -fprint-explicit-kinds+  hs-source-dirs:      bench+  default-language:    Haskell2010+  other-modules:+    DotProduct+  build-depends:+    base,+    fin,+    vec,+    vector,+    criterion >= 1.2.3.0 && <1.3