# Improving performance of mutable arrays using linear types

**URL:** <https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282>\
**Category:** Uncategorized\
**Created:** [September 3, 2024, 2:40pm UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282 "2024-09-03T14:40:09Z")\
**Posts on this page:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![Void](https://avatars.discourse-cdn.com/v4/letter/v/8baadc/32.png) [@Void](https://discourse.haskell.org/u/Void)\
**Post date:** [September 3, 2024, 2:40pm UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/1 "2024-09-03T14:40:09Z")

</div>

One of the most important applications of Linear Haskell is to allow pure mutable arrays and improve performance of algorithms involving arrays. However, in playing with Linear Haskell, an example caught my eyes: Suppose we implement Quicksort using the facilities provided by the linear-base package. Comparing the very naive implementation:

```haskell
qs :: Ord a => [a] -> [a]
qs [] = []
qs [x] = [x]
qs (x:xs) = qs [y|y <- xs, y < x] ++ x:[y <- xs, y >= x]

```

to the example implementation provided by the linear-base package: [linear-base/examples/Simple/Quicksort.hs at master · tweag/linear-base · GitHub](https://github.com/tweag/linear-base/blob/master/examples/Simple/Quicksort.hs)  
we would expect the linear implementation to perform better. However, the actual results shows that the naive algorithm actually performs better! On my device, to sort a random Int list of length 10^7, the naive algorithm takes 23s while the linear algorithm takes 70s (all tests done with -O2 compiler flag). Something is clearly wrong.

After some inspection at the code, I think the main culprit of the performance loss is allocation in the innermost loop. Consider the following code snippet:

```haskell
partition :: Array Int %1 -> Int -> Int -> Int -> (Array Int, Ur Int)
partition arr pivot lx rx
  | (rx < lx) = (arr, Ur (lx - 1))
  | otherwise =
      Array.read arr lx
        & \(Ur lVal, arr1) ->
          Array.read arr1 rx
            & \(Ur rVal, arr2) -> case (lVal <= pivot, pivot < rVal) of
              (True, True) -> partition arr2 pivot (lx + 1) (rx - 1)
              (True, False) -> partition arr2 pivot (lx + 1) rx
              (False, True) -> partition arr2 pivot lx (rx - 1)
              (False, False) ->
                swap arr2 lx rx
                  & \arr3 -> partition arr3 pivot (lx + 1) (rx - 1)

```

We see that tuples are spilled all over the place. Tuples are lifted types and adds a layer of indirection on the actual data, and creating them requires memory allocation. Furthermore, the `Ur` type is a data type instead of a newtype, which also causes allocation overhead. Those expensive allocations should be avoided as much as possible in the inner loop.

Here, I propose an approach to deal with this kind of overhead related to mutable array using linear types. The code can be found in [GitHub - Void-Skeleton/hstest: My personal repository for putting all sorts of Haskell tests](https://github.com/Void-Skeleton/hstest) (the code here is heavily inspired by the code from linear-base), where the main module of this test is ExampleL.hs. To summarize my approach, I used two tricks to optimize away the problems of tuples and data `Ur`.

1. The tuples can be trivially optimized away using unboxed tuples.
2. Instead of making `Ur` a GADT, we make `Ur` a `newtype`, with `newtype Ur a = Ur { unur :: a }`. You may be worried about the fact that a newtype constructor must always be linear. However, in an actual implementation, we hide that constructor from the module and only leave open the functions:

```haskell

ur :: a -> Ur a
ur = Ur {- Nonlinear construction -}

-- unur from newtype field

($-) :: (a %p -> b) %1 -> Ur a %1 -> b
($-) f = unsafeMultiplicity (\(Ur x) -> f x)

(&-) :: Ur a %1 -> (a %p -> b) %1 -> b
(&-) x f = f $- x

```

where `unsafeMultiplicity :: (a %p -> b) %1 -> a %q -> b` is an unsafe function obtained by wrapping `unsafeEqualityProof`. The exposed functions of the module corresponds perfectly to the axiomatic formulation of `Ur a`: A linear function from `Ur a` to `b` is just a regular function from `a` to `b`, while on the implementation level `Ur a` is nothing but `a`, removing the data constructor overhead.

With those optimizations done, a linear implementation of quicksort sorts 10^7 elements in 13s, 5 times faster than the implementation of linear-base and faster than the naive implementaion. Thus, I propose these tricks so as to make Linear Haskell a more viable choice for high-performance applications. I am also interested in the unsafe aspects of these tricks, and whether I missed something that causes safety problems in my implementation.

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 3, 2024, 2:50pm UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/2 "2024-09-03T14:50:07Z")

</div>

Amazing! I have also been surprised that `Ur` required an indirection and I support making it a `newtype` (assuming the API is genuinely type safe, which it seems to be to me).

---

<div class="post-metadata">

**Author:** ![danidiaz](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/danidiaz/32/92_2.png) [@danidiaz](https://discourse.haskell.org/u/danidiaz)\
**Post date:** [September 3, 2024, 6:11pm UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/3 "2024-09-03T18:11:46Z")

</div>

Out of curiosity, if we define `Ur` with a strict field, like

```haskell
data Ur a where
  Ur :: !a -> Ur a

```

Does that have any effect?

---

<div class="post-metadata">

**Author:** ![Vlix](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/vlix/32/1551_2.png) [@Vlix](https://discourse.haskell.org/u/Vlix)\
**Post date:** [September 3, 2024, 7:04pm UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/4 "2024-09-03T19:04:07Z")

</div>

Uhmmm, is this the implementation you used to benchmark?

> ```qs
> qs [] = []
> qs [x] = [x]
> qs (x:xs) = qs [y|y <- xs, y < x] ++ x:[y <- xs, y >= x]
> 
> ```

Because I think it’s wrong. IIUC, it should be:

```haskell
qs :: Ord a => [a] -> [a]
qs [] = []
qs [x] = [x]
qs (x:xs) =
    qs [y | y <- xs, y < x] ++ x : qs [y <- xs, y >= x]

```

---

<div class="post-metadata">

**Author:** ![Wxkj99](https://avatars.discourse-cdn.com/v4/letter/w/90ced4/32.png) [@Wxkj99](https://discourse.haskell.org/u/Wxkj99)\
**Post date:** [September 4, 2024, 12:31am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/5 "2024-09-04T00:31:16Z")

</div>

Wonderful performance! But I think it’s not worth letting the user use the unlifted types as they really cause trouble.

---

<div class="post-metadata">

**Author:** ![aspiwack](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/aspiwack/32/2240_2.png) [@aspiwack](https://discourse.haskell.org/u/aspiwack)\
**Post date:** [September 10, 2024, 2:54am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/6 "2024-09-10T02:54:56Z")

</div>

I’ve been pointed to this thread. Thank you for your interest. I’m glad more people are getting into linear types these days.

> [@Void](#):
>
> You may be worried about the fact that a newtype constructor must always be linear. However, in an actual implementation, we hide that constructor from the module and only leave open the functions:

Unfortunately, I don’t think that this is safe. This is no different than creating a newtype-Ur, so you’ll have the same unsafety issues (which I describe in [this section](https://www.tweag.io/blog/2024-01-18-linear-desugaring/#ur-cant-be-a-newtype) of a blog post I wrote earlier this year). Namely, in your case, that `const True $- destroyTheOneRing` will never actually destroy the one ring.

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 10, 2024, 4:12pm UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/7 "2024-09-10T16:12:44Z")

</div>

I think you’re saying that if `Ur` were a newtype with a special property obtained by hiding its constructors then its constructors wouldn’t actually be hidden to GHC and therefore GHC could apply linearity-violating transformations. Is that right?

---

<div class="post-metadata">

**Author:** ![tobz619](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tobz619/32/3125_2.png) [@tobz619](https://discourse.haskell.org/u/tobz619)\
**Post date:** [September 10, 2024, 7:50pm UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/8 "2024-09-10T19:50:30Z")

</div>

Sorry to be a noob but what the hell is `Ur`? :’)

---

<div class="post-metadata">

**Author:** ![mikeplus64](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/mikeplus64/32/3998_2.png) [@mikeplus64](https://discourse.haskell.org/u/mikeplus64)\
**Post date:** [September 11, 2024, 12:23am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/9 "2024-09-11T00:23:17Z")

</div>

Can you get around this with `seq` or a bang pattern? As in,

```haskell
unur :: Ur a %1 -> a
unur (Ur a) = case seq a () of () -> a -- or
unur (Ur a) = seq a a -- or
unur (Ur !a) = a
-- etc. I'm pretty sure these all have the same semantics... right?

```

Which I guess has its own different overhead than an indirection.

---

<div class="post-metadata">

**Author:** ![aspiwack](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/aspiwack/32/2240_2.png) [@aspiwack](https://discourse.haskell.org/u/aspiwack)\
**Post date:** [September 11, 2024, 12:53am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/10 "2024-09-11T00:53:40Z")

</div>

> [@tomjaguarpaw](#):
>
> I think you’re saying that if `Ur` were a newtype with a special property obtained by hiding its constructors then its constructors wouldn’t actually be hidden to GHC and therefore GHC could apply linearity-violating transformations. Is that right?

I’m not sure what you mean, maybe? The point is that `\(Ur x) -> f x`, in the definition of `($-)` is compiled as `\x -> f x` (up to some types shenanigans). Not sure if it counts as a transformation, it’s just the semantics of the thing. And for or case, it does mean that `f` is free to drop `x`.

> [@tobz619](#):
>
> Sorry to be a noob but what the hell is `Ur`? :’)

`Ur a` is a value of type `a` which is unrestricted (aka, slightly abusively, non-linear) even if the `Ur a` itself is linear. This is the Haskell equivalent to the `!A` of linear logic. Another (formalist) way to say it, is that `Ur a %1 -> b` is isomorphic to `a -> b`.

> [@mikeplus64](#):
>
> Can you get around this with `seq` or a bang pattern?

I don’t know. I’ve convinced myself at some point that this wasn’t enough. But maybe I’m wrong: I don’t recall my argument.

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 11, 2024, 7:32am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/11 "2024-09-11T07:32:48Z")

</div>

> [@aspiwack](#):
>
> > [@tomjaguarpaw](#):
> >
> > I think you’re saying that if `Ur` were a newtype with a special property obtained by hiding its constructors then its constructors wouldn’t actually be hidden to GHC and therefore GHC could apply linearity-violating transformations. Is that right?
> 
> I’m not sure what you mean, maybe? The point is that `\(Ur x) -> f x`, in the definition of `($-)` is compiled as `\x -> f x` (up to some types shenanigans). Not sure if it counts as a transformation, it’s just the semantics of the thing. And for or case, it does mean that `f` is free to drop `x`.

Hmm, now that I’ve tried to think about it some more I don’t understand why compiling `($-)` to `\f x -> f x` is actually bad. Why shouldn’t it drop `x`? You can only construct an `Ur a` from an `a` non-linearly, so you’re not violating anyone’s expectations if you drop or duplicate the `a`, are you?

For example, I can write

```haskell
f :: Ur x %1 -> ()
f ux = (\_ -> ()) $- ux

```

to drop `x`, and

```haskell
g :: Ur x %1 -> (x, x)
g ux = (\x -> (x, x)) $- ux

```

or even

```haskell
h :: Ur x %1 -> Ur (x, x)
h = (\x -> ur (x, x)) $- ux

```

What’s wrong with that? “The `Ur` constructor is not forced”, indeed, because there is no `Ur` constructor! But I don’t see why that’s bad. What guarantees does being able to do that violate?

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 11, 2024, 7:39am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/12 "2024-09-11T07:39:14Z")

</div>

> [@mikeplus64](#):
>
> ```haskell
> unur :: Ur a %1 -> a
> unur (Ur a) = case seq a () of () -> a -- or
> unur (Ur a) = seq a a -- or
> unur (Ur !a) = a
> -- etc. I'm pretty sure these all have the same semantics... right?
> 
> ```

These are all no-ops.

The first means "when you come to evaluate the result (of `unur (Ur a)`) first evaluate `seq a ()` to a `()`, which requires evaluating `a` first. But `a` is the result, so evaluating `a` before returning the result is a no-op.

The second means “when you come to evaluate the result evaluate `a` beforehand”, but again `a` is the result, so this is a no op.

The third is indeed just the second.

---

<div class="post-metadata">

**Author:** ![aspiwack](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/aspiwack/32/2240_2.png) [@aspiwack](https://discourse.haskell.org/u/aspiwack)\
**Post date:** [September 12, 2024, 1:10am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/13 "2024-09-12T01:10:58Z")

</div>

> [@tomjaguarpaw](#):
>
> What’s wrong with that? “The `Ur` constructor is not forced”, indeed, because there is no `Ur` constructor! But I don’t see why that’s bad. What guarantees does being able to do that violate?

The problem is that `x : Ur a` is a thunk which is allowed to contain linear values which must be consumed once. Only when I force the `Ur a` thunk to reveal an `Ur` constructor do I actually consume these values.

Consider:

```haskell
lotr :: Ur Peace %1 -> ()
lotr destroyTheOneRing = const () $- destroyTheOneRing

```

This violates the linearity condition that `destroyTheOneRing` must be consumed. It never is. Maybe `destroyTheOneRing` refers to a file or something, in which case the file is never closed.

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 12, 2024, 7:04am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/14 "2024-09-12T07:04:57Z")

</div>

> [@aspiwack](#):
>
> The problem is that `x : Ur a` is a thunk which is allowed to contain linear values which must be consumed once.

Is it? How can it possibly when its constructor is non-linear? Can you give an example?

---

<div class="post-metadata">

**Author:** ![aspiwack](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/aspiwack/32/2240_2.png) [@aspiwack](https://discourse.haskell.org/u/aspiwack)\
**Post date:** [September 12, 2024, 8:44am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/15 "2024-09-12T08:44:12Z")

</div>

Something like:

```haskell
f :: A %1 -> B
f x =
  let
    u :: Ur Int -- thunk whose free variables include x
    u = consume x `lseq` Ur 57
  in
  …u …

```

The idea is that the `Ur a` thunk is linear, whereas the value of type `a` it holds isn’t. And as any linear thunk, it may contain arbitrary linear stuff in its closure.

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 12, 2024, 10:12am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/16 "2024-09-12T10:12:17Z")

</div>

Oh, how interesting! To avoid having to know what `lseq` is, I think we can write the same example as

```haskell
f :: A %1 -> B
f x =
  let
    u :: Ur Int -- thunk whose free variables include x
    u = case consume x of () -> Ur 57
  in
  … u …

```

In which case my next guess is that making the “continuation” strict in its argument is probably safe

```haskell
($-) :: (a %p -> b) %1 -> Ur a %1 -> b
($-) f = unsafeMultiplicity (\(Ur !x) -> f x)

```

(which is probably what @mikeplus64’s intuition was getting at)

---

<div class="post-metadata">

**Author:** ![aspiwack](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/aspiwack/32/2240_2.png) [@aspiwack](https://discourse.haskell.org/u/aspiwack)\
**Post date:** [September 13, 2024, 1:42am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/17 "2024-09-13T01:42:03Z")

</div>

> [@tomjaguarpaw](#):
>
> In which case my next guess is that making the “continuation” strict in its argument is probably safe

Maybe. I’m not confident about it (but neither am I confident that it’d be unsafe). It would require some careful proof. I’m not sure it’s worth it in recent GHCs though, considering that `Ur` is usually unboxed.

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 13, 2024, 7:26am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/18 "2024-09-13T07:26:04Z")

</div>

> [@aspiwack](#):
>
> considering that `Ur` is usually unboxed.

This `Ur`? [Data.Unrestricted.Linear](https://www.stackage.org/haddock/lts-22.34/linear-base-0.4.0/Data-Unrestricted-Linear.html#t:Ur) How is it unboxed? The definition itself is of a boxed type, isn’t it? Do you mean the GHC can often apply an unboxing transformation to it? Perhaps, but this thread is predicated on the observation that unboxing it manually (plus getting rid of the additional tag, i.e. converting it to a `newtype`) picks up impressive performance gains.

---

<div class="post-metadata">

**Author:** ![aspiwack](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/aspiwack/32/2240_2.png) [@aspiwack](https://discourse.haskell.org/u/aspiwack)\
**Post date:** [September 17, 2024, 8:54am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/19 "2024-09-17T08:54:38Z")

</div>

That GHC applies the unboxing transformation.

I think that what we’re seeing here is that older versions of GHC fail to optimize this code properly. Whereas newer versions do it easily. Per @tbagrel1 's [post on the other thread](http://discourse.haskell.org/t/linear-haskell-quicksort-performance/10280/9).

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 17, 2024, 10:14am UTC](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282/20 "2024-09-17T10:14:01Z")

</div>

That’s great if so! Although it says

> [@Linear Haskell QuickSort Performance](http://discourse.haskell.org/t/linear-haskell-quicksort-performance/10280/9):
>
> Of course, most `Ur` were still there, but that was to be expected.

[Next page](https://discourse.haskell.org/t/improving-performance-of-mutable-arrays-using-linear-types/10282.md?page=2)