More generic push arrays 1/2 by Divesh-Otwani · Pull Request #287 · tweag/linear-base

Divesh-Otwani · 2021-01-04T15:10:11Z

This PR flushes out the design laid out in the better-push-array branch. [In an effort to avoid plagiarism: note that all of these are @aspiwack's ideas.] We represent push arrays with this clever little rank-2 thing:

data Array a where
  Array :: (forall m. Monoid m => (a -> m) -> m) %1-> Array a

that takes a polymorphic conversion to a monoid for some element, and creates a monoid. This way it represents the monoidal concatenation of a certain natural (including zero) number of as, in some unknown order.

We instantiate this with a function that takes an a and makes it an ArrayWriter a:

data ArrayWriter a where
  ArrayWriter :: (DArray a %1-> ()) %1-> !Int -> ArrayWriter a

which holds the ingredients needed to write some number of elements, without holding the space to do so.

This is part 1/2 because I still have to add the fold functions.

utdemir · 2021-01-05T05:19:24Z

-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)])


I'm not sure, but in my experience foldl is rarely the most efficient fold. Probably I'd go with foldl'.

We discussed, at some point somewhere, making foldl be the strict version, and having another name for the lazy fold. Probably we should just go for it.

In this case, though, this ought to be a simpler foldMap do we have foldMap?

We can't use a linear foldMap without changing the type of Push and Pull to hold Int %1-> a and (a %1-> m) -> m respectively. I will usePrelude.foldMap.

Or did you mean a foldMap on Pull arrays? @aspiwack

I meant foldMap on lists. But you are right that there is some tension in the types. Let's forget about this for now.

utdemir · 2021-01-05T05:23:47Z

+-- must follow so that we can release a safe API.
+
+emptyWriter :: ArrayWriter a
+emptyWriter = ArrayWriter (Unsafe.toLinear (const ())) 0


Unsafe call here assumes that we can just forget about the DArray. I think this is the case; but it might worth a comment here. (I think every unsafe call deserves a comment unless incredibly obvious.)

There shouldn't be an Unsafe.toLinear in this module. If we are missing a way to consume an empty destination array, then let's add it to the destination array module.

I'll make a safe empty DArray consumer with HasCallStack.

utdemir · 2021-01-05T05:29:10Z

+  (<>) x y = append x y
+
+instance Semigroup (Array a) where
+  (<>) = append


This is a purely stylistic choice, so feel free to ignore this; but I'd just inline the append here, I don't see a much need for a separate function and the fewer names the better.

Same goes with mempty and the variants for ArrayWriter.

I like it because it's a tiny bit more DRY even though the chance of changing the implementation is close to zero.

aspiwack · 2021-01-05T07:53:22Z

-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)])


We discussed, at some point somewhere, making foldl be the strict version, and having another name for the lazy fold. Probably we should just go for it.

aspiwack · 2021-01-05T07:54:23Z

-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)])


In this case, though, this ought to be a simpler foldMap do we have foldMap?

aspiwack · 2021-01-05T07:58:03Z

-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"


Suggested change

| n < 0 = error "Making negative length push array"

| n < 0 = error "Making a negative length push array"

aspiwack · 2021-01-05T08:10:04Z

+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))


Base has an stimes function for this. Maybe we should have one too?

Array $ \makeA -> stimes (makeA x) might be more efficient if the stimes implementation for ArrayWriter could be more efficient. However, I don't want to change Monoid in this PR.

As you wish, but I think it's fine to lazily add stuff to the library (though I'm sensitive to the argument that changing a type class is not a cheap action, and may need to be done carefully).

It was not really about efficiency (though it may be), but about clarity. We can do this in a separate PR.

aspiwack · 2021-01-05T08:13:42Z

+-- 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.


Sure, but, on the other hand, you cannot not consume them (try to forget consume or something). That's what linearity does for you. The unsafe IO is (if I haven't messed up) fully encapsulated in the DArray abstraction. So types guarantee that you can't get this wrong. Therefore, this comment is superfluous

Suggested change

-- 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.

Yes, I see xD *facepalms himself*. There's no way to write ((),()) %1-> () without using something unsafe that doesn't force the evaluation of both tuples.

aspiwack · 2021-01-05T08:15:34Z

+-- must follow so that we can release a safe API.
+
+emptyWriter :: ArrayWriter a
+emptyWriter = ArrayWriter (Unsafe.toLinear (const ())) 0


There shouldn't be an Unsafe.toLinear in this module. If we are missing a way to consume an empty destination array, then let's add it to the destination array module.

aspiwack · 2021-01-06T08:38:42Z

+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 = ()


You know what? I don't think it's safe. We at least need to seq ds like this:

Suggested change

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 = ()

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 = ds `seq` ()

But generally speaking, I'm wondering if we shouldn't replace newtype DArray a = DArray (MVector …) with data DArray a where { DArray :: MVector … -> DArray a }. It adds an indirection. But it will save some Unsafe.toLinear presumably. Maybe most. This may considerably reduce the kernel of trust, here.

I'll make that ^ an issue for later.

Divesh-Otwani requested review from aspiwack and utdemir January 4, 2021 15:10

More generic push arrays

a295889

Divesh-Otwani force-pushed the better-push-arrays-2 branch from 2012c45 to a295889 Compare January 4, 2021 15:27

utdemir reviewed Jan 5, 2021

View reviewed changes

aspiwack reviewed Jan 5, 2021

View reviewed changes

Cleanups from PR review

f4b1f24

Divesh-Otwani requested a review from aspiwack January 5, 2021 18:08

aspiwack reviewed Jan 6, 2021

View reviewed changes

Divesh-Otwani mentioned this pull request Jan 6, 2021

Push arrays/fold #288

Merged

Safe dropping of empty destination arrays

e442c55

aspiwack approved these changes Jan 6, 2021

View reviewed changes

Divesh-Otwani merged commit d0863c6 into master Jan 6, 2021

Divesh-Otwani deleted the better-push-arrays-2 branch January 6, 2021 15:44

aspiwack mentioned this pull request Jan 6, 2021

Destination array newtype wrapper #289

Closed

	\| n < 0 = error "Making negative length push array"
	\| n < 0 = error "Making a negative length push array"

Conversation

Divesh-Otwani commented Jan 4, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Divesh-Otwani Jan 5, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Divesh-Otwani Jan 5, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Divesh-Otwani Jan 5, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Divesh-Otwani Jan 5, 2021 •

edited

Loading

Divesh-Otwani Jan 5, 2021 •

edited

Loading

Divesh-Otwani Jan 5, 2021 •

edited

Loading