|
1 | | -{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} |
2 | 1 | {-# LANGUAGE DerivingVia #-} |
3 | 2 | {-# LANGUAGE GADTs #-} |
4 | 3 | {-# LANGUAGE LinearTypes #-} |
|
11 | 10 | -- allocated for an array. See @Data.Array.Polarized@. |
12 | 11 | -- |
13 | 12 | -- This module is designed to be imported qualified as @Push@. |
14 | | -module Data.Array.Polarized.Push where |
| 13 | +module Data.Array.Polarized.Push |
| 14 | + ( Array(..) |
| 15 | + , alloc |
| 16 | + , make |
| 17 | + ) |
| 18 | +where |
15 | 19 |
|
16 | | --- XXX: it might be better to hide the data constructor, in case we wish to |
17 | | --- change the implementation. |
18 | | - |
19 | | -import Data.Array.Destination (DArray) |
20 | | -import qualified Data.Array.Destination as DArray |
21 | 20 | import qualified Data.Functor.Linear as Data |
| 21 | +import qualified Data.Array.Destination as DArray |
| 22 | +import Data.Array.Destination (DArray) |
22 | 23 | import Data.Vector (Vector) |
23 | | -import Prelude.Linear |
24 | 24 | import qualified Prelude |
| 25 | +import Prelude.Linear |
| 26 | +import GHC.Stack |
| 27 | + |
25 | 28 |
|
26 | | --- TODO: the below isn't really true yet since no friendly way of constructing |
27 | | --- a PushArray directly is given yet (see issue #62), but the spirit holds. |
28 | | --- TODO: There's also a slight lie in that one might want to consume a |
29 | | --- PushArray into a commutative monoid, for instance summing all the elements, |
30 | | --- and this is not yet possible, although it should be. |
| 29 | +-- The Types |
| 30 | +------------------------------------------------------------------------------- |
31 | 31 |
|
32 | 32 | -- | Push arrays are un-allocated finished arrays. These are finished |
33 | 33 | -- computations passed along or enlarged until we are ready to allocate. |
34 | 34 | data Array a where |
| 35 | + Array :: (forall m. Monoid m => (a -> m) -> m) %1-> Array a |
| 36 | + -- Developer notes: |
| 37 | + -- |
| 38 | + -- Think of @(a -> m)@ as something that writes an @a@ and think of |
| 39 | + -- @((a -> m) -> m)@ as something that takes a way to write a single element |
| 40 | + -- and writes and concatenates all elements. |
| 41 | + -- |
| 42 | + -- Also, note that in this formulation we don't know the length beforehand. |
| 43 | + |
| 44 | +data ArrayWriter a where |
| 45 | + ArrayWriter :: (DArray a %1-> ()) %1-> !Int -> ArrayWriter a |
35 | 46 | -- The second parameter is the length of the @DArray@ |
36 | | - Array :: (forall b. (a %1-> b) -> DArray b %1-> ()) %1-> Int -> Array a |
37 | | - deriving Prelude.Semigroup via NonLinear (Array a) |
38 | 47 |
|
39 | | -instance Data.Functor Array where |
40 | | - fmap f (Array k n) = Array (\g dest -> k (g . f) dest) n |
41 | 48 |
|
42 | | -instance Semigroup (Array a) where |
43 | | - (<>) = append |
| 49 | +-- API |
| 50 | +------------------------------------------------------------------------------- |
44 | 51 |
|
45 | | --- XXX: the use of Vector in the type of alloc is temporary (see also |
46 | | --- "Data.Array.Destination") |
47 | 52 | -- | Convert a push array into a vector by allocating. This would be a common |
48 | 53 | -- end to a computation using push and pull arrays. |
49 | 54 | alloc :: Array a %1-> Vector a |
50 | | -alloc (Array k n) = DArray.alloc n (k id) |
| 55 | +alloc (Array k) = allocArrayWriter $ k singletonWriter where |
| 56 | + singletonWriter :: a -> ArrayWriter a |
| 57 | + singletonWriter a = ArrayWriter (DArray.fill a) 1 |
| 58 | + |
| 59 | + allocArrayWriter :: ArrayWriter a %1-> Vector a |
| 60 | + allocArrayWriter (ArrayWriter writer len) = DArray.alloc len writer |
51 | 61 |
|
52 | 62 | -- | @`make` x n@ creates a constant push array of length @n@ in which every |
53 | 63 | -- element is @x@. |
54 | | -make :: a -> Int -> Array a |
55 | | -make x n = Array (\k -> DArray.replicate (k x)) n |
| 64 | +make :: HasCallStack => a -> Int -> Array a |
| 65 | +make x n |
| 66 | + | n < 0 = error "Making a negative length push array" |
| 67 | + | otherwise = Array (\makeA -> mconcat $ Prelude.replicate n (makeA x)) |
| 68 | + |
| 69 | + |
| 70 | +-- # Instances |
| 71 | +------------------------------------------------------------------------------- |
| 72 | + |
| 73 | +instance Data.Functor Array where |
| 74 | + fmap f (Array k) = Array (\g -> k (\x -> (g (f x)))) |
| 75 | + |
| 76 | +instance Prelude.Semigroup (Array a) where |
| 77 | + (<>) x y = append x y |
| 78 | + |
| 79 | +instance Semigroup (Array a) where |
| 80 | + (<>) = append |
| 81 | + |
| 82 | +instance Prelude.Monoid (Array a) where |
| 83 | + mempty = empty |
| 84 | + |
| 85 | +instance Monoid (Array a) where |
| 86 | + mempty = empty |
| 87 | + |
| 88 | +empty :: Array a |
| 89 | +empty = Array (\_ -> mempty) |
56 | 90 |
|
57 | | --- | Concatenate two push arrays. |
58 | 91 | append :: Array a %1-> Array a %1-> Array a |
59 | | -append (Array kl nl) (Array kr nr) = |
60 | | - Array |
61 | | - (\f dest -> parallelApply f kl kr (DArray.split nl dest)) |
62 | | - (nl+nr) |
63 | | - where |
64 | | - parallelApply :: (a %1-> b) -> ((a %1-> b) -> DArray b %1-> ()) %1-> ((a %1-> b) -> DArray b %1-> ()) %1-> (DArray b, DArray b) %1-> () |
65 | | - parallelApply f' kl' kr' (dl, dr) = kl' f' dl <> kr' f' dr |
| 92 | +append (Array k1) (Array k2) = Array (\writeA -> k1 writeA <> k2 writeA) |
| 93 | + |
| 94 | +instance Prelude.Semigroup (ArrayWriter a) where |
| 95 | + (<>) x y = addWriters x y |
| 96 | + |
| 97 | +instance Prelude.Monoid (ArrayWriter a) where |
| 98 | + mempty = emptyWriter |
| 99 | + |
| 100 | +instance Semigroup (ArrayWriter a) where |
| 101 | + (<>) = addWriters |
| 102 | + |
| 103 | +instance Monoid (ArrayWriter a) where |
| 104 | + mempty = emptyWriter |
| 105 | + |
| 106 | +addWriters :: ArrayWriter a %1-> ArrayWriter a %1-> ArrayWriter a |
| 107 | +addWriters (ArrayWriter k1 l1) (ArrayWriter k2 l2) = |
| 108 | + ArrayWriter |
| 109 | + (\darr -> |
| 110 | + (DArray.split l1 darr) & \(darr1,darr2) -> consume (k1 darr1, k2 darr2)) |
| 111 | + (l1+l2) |
| 112 | + |
| 113 | +emptyWriter :: ArrayWriter a |
| 114 | +emptyWriter = ArrayWriter DArray.dropEmpty 0 |
| 115 | +-- Remark. @emptyWriter@ assumes we can split a destination array at 0. |
| 116 | + |
0 commit comments