diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,4 @@ +# Revision history for boring +## 0 + +- First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/bench/Bench.hs b/bench/Bench.hs new file mode 100644 --- /dev/null +++ b/bench/Bench.hs @@ -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) + ] + ] diff --git a/bench/DotProduct.hs b/bench/DotProduct.hs new file mode 100644 --- /dev/null +++ b/bench/DotProduct.hs @@ -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) diff --git a/src/Data/Vec/Lazy.hs b/src/Data/Vec/Lazy.hs new file mode 100644 --- /dev/null +++ b/src/Data/Vec/Lazy.hs @@ -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) diff --git a/src/Data/Vec/Lazy/Inline.hs b/src/Data/Vec/Lazy/Inline.hs new file mode 100644 --- /dev/null +++ b/src/Data/Vec/Lazy/Inline.hs @@ -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) diff --git a/src/Data/Vec/Pull.hs b/src/Data/Vec/Pull.hs new file mode 100644 --- /dev/null +++ b/src/Data/Vec/Pull.hs @@ -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 diff --git a/test/Inspection.hs b/test/Inspection.hs new file mode 100644 --- /dev/null +++ b/test/Inspection.hs @@ -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 () diff --git a/vec.cabal b/vec.cabal new file mode 100644 --- /dev/null +++ b/vec.cabal @@ -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 +maintainer: Oleg.Grenrus +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