From a29588922c2310cd5a47368df2e9207954efad8c Mon Sep 17 00:00:00 2001 From: Divesh Otwani Date: Mon, 4 Jan 2021 07:56:40 -0500 Subject: [PATCH 1/3] More generic push arrays --- src/Data/Array/Polarized.hs | 6 +- src/Data/Array/Polarized/Push.hs | 121 +++++++++++++++++++++++-------- 2 files changed, 93 insertions(+), 34 deletions(-) diff --git a/src/Data/Array/Polarized.hs b/src/Data/Array/Polarized.hs index be47c33a..81d539d6 100644 --- a/src/Data/Array/Polarized.hs +++ b/src/Data/Array/Polarized.hs @@ -99,11 +99,11 @@ module Data.Array.Polarized ) where -import qualified Data.Array.Destination as DArray import qualified Data.Array.Polarized.Pull.Internal as Pull import qualified Data.Array.Polarized.Pull as Pull import qualified Data.Array.Polarized.Push as Push import Prelude.Linear +import qualified Prelude import Data.Vector (Vector) -- DEVELOPER NOTE: @@ -129,7 +129,9 @@ import Data.Vector (Vector) -- | Convert a pull array into a push array. -- NOTE: this does NOT require allocation and can be in-lined. transfer :: Pull.Array a %1-> Push.Array a -transfer (Pull.Array f n) = Push.Array (\g -> DArray.fromFunction (\i -> g (f i))) n +transfer (Pull.Array f n) = + Push.Array + (\k -> Prelude.foldl (\m i -> m <> (k (f i))) mempty [0..(n-1)]) -- | This is a shortcut convenience function -- for @transfer . Pull.fromVector@. diff --git a/src/Data/Array/Polarized/Push.hs b/src/Data/Array/Polarized/Push.hs index c5bb6036..712d4046 100644 --- a/src/Data/Array/Polarized/Push.hs +++ b/src/Data/Array/Polarized/Push.hs @@ -1,4 +1,3 @@ -{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LinearTypes #-} @@ -11,55 +10,113 @@ -- allocated for an array. See @Data.Array.Polarized@. -- -- This module is designed to be imported qualified as @Push@. -module Data.Array.Polarized.Push where +module Data.Array.Polarized.Push + ( Array(..) + , alloc + , make + ) +where --- XXX: it might be better to hide the data constructor, in case we wish to --- change the implementation. - -import Data.Array.Destination (DArray) -import qualified Data.Array.Destination as DArray import qualified Data.Functor.Linear as Data +import qualified Data.Array.Destination as DArray +import Data.Array.Destination (DArray) import Data.Vector (Vector) -import Prelude.Linear import qualified Prelude +import qualified Unsafe.Linear as Unsafe +import Prelude.Linear +import GHC.Stack + --- TODO: the below isn't really true yet since no friendly way of constructing --- a PushArray directly is given yet (see issue #62), but the spirit holds. --- TODO: There's also a slight lie in that one might want to consume a --- PushArray into a commutative monoid, for instance summing all the elements, --- and this is not yet possible, although it should be. +-- The Types +------------------------------------------------------------------------------- -- | Push arrays are un-allocated finished arrays. These are finished -- computations passed along or enlarged until we are ready to allocate. data Array a where + Array :: (forall m. Monoid m => (a -> m) -> m) %1-> Array a + -- Developer notes: + -- + -- Think of @(a -> m)@ as something that writes an @a@ and think of + -- @((a -> m) -> m)@ as something that takes a way to write a single element + -- and writes and concatenates all elements. + -- + -- Also, note that in this formulation we don't know the length beforehand. + +data ArrayWriter a where + ArrayWriter :: (DArray a %1-> ()) %1-> !Int -> ArrayWriter a -- The second parameter is the length of the @DArray@ - Array :: (forall b. (a %1-> b) -> DArray b %1-> ()) %1-> Int -> Array a - deriving Prelude.Semigroup via NonLinear (Array a) -instance Data.Functor Array where - fmap f (Array k n) = Array (\g dest -> k (g . f) dest) n -instance Semigroup (Array a) where - (<>) = append +-- API +------------------------------------------------------------------------------- --- XXX: the use of Vector in the type of alloc is temporary (see also --- "Data.Array.Destination") -- | Convert a push array into a vector by allocating. This would be a common -- end to a computation using push and pull arrays. alloc :: Array a %1-> Vector a -alloc (Array k n) = DArray.alloc n (k id) +alloc (Array k) = allocArrayWriter $ k singletonWriter where + singletonWriter :: a -> ArrayWriter a + singletonWriter a = ArrayWriter (DArray.fill a) 1 + + allocArrayWriter :: ArrayWriter a %1-> Vector a + allocArrayWriter (ArrayWriter writer len) = DArray.alloc len writer -- | @`make` x n@ creates a constant push array of length @n@ in which every -- element is @x@. -make :: a -> Int -> Array a -make x n = Array (\k -> DArray.replicate (k x)) n +make :: HasCallStack => a -> Int -> Array a +make x n + | n < 0 = error "Making negative length push array" + | otherwise = Array (\makeA -> mconcat $ Prelude.replicate n (makeA x)) + + +-- # Instances +------------------------------------------------------------------------------- + +instance Data.Functor Array where + fmap f (Array k) = Array (\g -> k (\x -> (g (f x)))) + +instance Prelude.Semigroup (Array a) where + (<>) x y = append x y + +instance Semigroup (Array a) where + (<>) = append + +instance Prelude.Monoid (Array a) where + mempty = empty + +instance Monoid (Array a) where + mempty = empty + +empty :: Array a +empty = Array (\_ -> mempty) --- | Concatenate two push arrays. append :: Array a %1-> Array a %1-> Array a -append (Array kl nl) (Array kr nr) = - Array - (\f dest -> parallelApply f kl kr (DArray.split nl dest)) - (nl+nr) - where - parallelApply :: (a %1-> b) -> ((a %1-> b) -> DArray b %1-> ()) %1-> ((a %1-> b) -> DArray b %1-> ()) %1-> (DArray b, DArray b) %1-> () - parallelApply f' kl' kr' (dl, dr) = kl' f' dl <> kr' f' dr +append (Array k1) (Array k2) = Array (\writeA -> k1 writeA <> k2 writeA) + +instance Prelude.Semigroup (ArrayWriter a) where + (<>) x y = addWriters x y + +instance Prelude.Monoid (ArrayWriter a) where + mempty = emptyWriter + +instance Semigroup (ArrayWriter a) where + (<>) = addWriters + +instance Monoid (ArrayWriter a) where + mempty = emptyWriter + +addWriters :: ArrayWriter a %1-> ArrayWriter a %1-> ArrayWriter a +addWriters (ArrayWriter k1 l1) (ArrayWriter k2 l2) = + ArrayWriter + (\darr -> + (DArray.split l1 darr) & \(darr1,darr2) -> consume (k1 darr1, k2 darr2)) + (l1+l2) +-- Remark. In order for the function above to work, consume must forcibly +-- evaluate both tuples. If it was lazy, then we might not actually perform +-- @k1@ or @k2@ and the unsafe IO won't get done. In general, this makes me +-- think we haven't spelled out the careful rules of what consuming functions +-- must follow so that we can release a safe API. + +emptyWriter :: ArrayWriter a +emptyWriter = ArrayWriter (Unsafe.toLinear (const ())) 0 +-- Remark. @emptyWriter@ assumes we can split a destination array at 0. + From f4b1f241373eefe765f89766ab437a9b47609326 Mon Sep 17 00:00:00 2001 From: Divesh Otwani Date: Tue, 5 Jan 2021 13:06:58 -0500 Subject: [PATCH 2/3] Cleanups from PR review --- src/Data/Array/Destination.hs | 9 +++++++++ src/Data/Array/Polarized.hs | 5 ++--- src/Data/Array/Polarized/Push.hs | 10 ++-------- 3 files changed, 13 insertions(+), 11 deletions(-) diff --git a/src/Data/Array/Destination.hs b/src/Data/Array/Destination.hs index f671897e..2a05ade7 100644 --- a/src/Data/Array/Destination.hs +++ b/src/Data/Array/Destination.hs @@ -123,6 +123,7 @@ module Data.Array.Destination , mirror , fromFunction , fill + , dropEmpty ) where @@ -179,6 +180,14 @@ fill = Unsafe.toLinear2 unsafeFill else unsafeDupablePerformIO Prelude.$ MVector.write ds 0 a +-- | @dropEmpty dest@ consumes and empty array and fails otherwise. +dropEmpty :: HasCallStack => DArray a %1-> () +dropEmpty = Unsafe.toLinear unsafeDrop where + unsafeDrop :: DArray a -> () + unsafeDrop (DArray ds) + | MVector.length ds > 0 = error "Destination.dropEmpty on non-empty array." + | otherwise = () + -- | @'split' n dest = (destl, destr)@ such as @destl@ has length @n@. -- -- 'split' is total: if @n@ is larger than the length of @dest@, then diff --git a/src/Data/Array/Polarized.hs b/src/Data/Array/Polarized.hs index 81d539d6..35cd71ce 100644 --- a/src/Data/Array/Polarized.hs +++ b/src/Data/Array/Polarized.hs @@ -102,8 +102,8 @@ module Data.Array.Polarized import qualified Data.Array.Polarized.Pull.Internal as Pull import qualified Data.Array.Polarized.Pull as Pull import qualified Data.Array.Polarized.Push as Push +import qualified Data.Foldable as NonLinear import Prelude.Linear -import qualified Prelude import Data.Vector (Vector) -- DEVELOPER NOTE: @@ -130,8 +130,7 @@ import Data.Vector (Vector) -- NOTE: this does NOT require allocation and can be in-lined. transfer :: Pull.Array a %1-> Push.Array a transfer (Pull.Array f n) = - Push.Array - (\k -> Prelude.foldl (\m i -> m <> (k (f i))) mempty [0..(n-1)]) + Push.Array (\k -> NonLinear.foldMap' (\x -> k (f x)) [0..(n-1)]) -- | This is a shortcut convenience function -- for @transfer . Pull.fromVector@. diff --git a/src/Data/Array/Polarized/Push.hs b/src/Data/Array/Polarized/Push.hs index 712d4046..437c634d 100644 --- a/src/Data/Array/Polarized/Push.hs +++ b/src/Data/Array/Polarized/Push.hs @@ -22,7 +22,6 @@ import qualified Data.Array.Destination as DArray import Data.Array.Destination (DArray) import Data.Vector (Vector) import qualified Prelude -import qualified Unsafe.Linear as Unsafe import Prelude.Linear import GHC.Stack @@ -64,7 +63,7 @@ alloc (Array k) = allocArrayWriter $ k singletonWriter where -- element is @x@. make :: HasCallStack => a -> Int -> Array a make x n - | n < 0 = error "Making negative length push array" + | n < 0 = error "Making a negative length push array" | otherwise = Array (\makeA -> mconcat $ Prelude.replicate n (makeA x)) @@ -110,13 +109,8 @@ addWriters (ArrayWriter k1 l1) (ArrayWriter k2 l2) = (\darr -> (DArray.split l1 darr) & \(darr1,darr2) -> consume (k1 darr1, k2 darr2)) (l1+l2) --- Remark. In order for the function above to work, consume must forcibly --- evaluate both tuples. If it was lazy, then we might not actually perform --- @k1@ or @k2@ and the unsafe IO won't get done. In general, this makes me --- think we haven't spelled out the careful rules of what consuming functions --- must follow so that we can release a safe API. emptyWriter :: ArrayWriter a -emptyWriter = ArrayWriter (Unsafe.toLinear (const ())) 0 +emptyWriter = ArrayWriter DArray.dropEmpty 0 -- Remark. @emptyWriter@ assumes we can split a destination array at 0. From e442c5593bbe6ad3c727c2db1cdf0403a96f80dd Mon Sep 17 00:00:00 2001 From: Divesh Otwani Date: Wed, 6 Jan 2021 10:25:52 -0500 Subject: [PATCH 3/3] Safe dropping of empty destination arrays --- src/Data/Array/Destination.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Array/Destination.hs b/src/Data/Array/Destination.hs index 2a05ade7..9d8745d3 100644 --- a/src/Data/Array/Destination.hs +++ b/src/Data/Array/Destination.hs @@ -186,7 +186,7 @@ dropEmpty = Unsafe.toLinear unsafeDrop where unsafeDrop :: DArray a -> () unsafeDrop (DArray ds) | MVector.length ds > 0 = error "Destination.dropEmpty on non-empty array." - | otherwise = () + | otherwise = ds `seq` () -- | @'split' n dest = (destl, destr)@ such as @destl@ has length @n@. --