• Prelude.Linear should not define functions, and should only re-export functions
• Organize Foreign.Marshall.Pure into sections

The current type of Push Arrays does not allow some operations which ought to be possible for a Push Array: for instance folding into a monoid or unzipping. It seems that the DArray ->. () ought to be generalised somehow; at the moment, the only way to consume a Push Array is to allocate.

And does this help us basically get a newtype without the unsafeness b/c of non-strictness and coersions?

It's possible to have some empty mutable linear data structures but unsafeCoerceing unit or something, and internally making sure nothing crashes.

This is something which has bothered everyone for months. It resurfaced recently in our internal discussion channels. We still don't have a clear solution.

The problem: Unrestricted, while a perfectly descriptive name, is very long. And considering how often this type is referred to in type signatures (and its constructor in function definition), we really want a shorter name. It's for everybody's sanity.

This naming issue can also be accompanied by a reflection of how to name of the accompanying, and commonly useful

data X s a where
  X :: s #-> a -> X s a

(the fields may be in the reverse order, I don't care much either way)

Here is a list of all the proposals that have been mooted that I can remember

• Many: but since it's already used for the name of the multiplicity, it invites many conflicts which are likely to be unpleasant.
• Bang after the fact that Unrestricted a is write !a in traditional linear logic literature. But it's fairly meaningless, if you don't know that notation.
• Poly: after polynomial (linear: I must consume once, quadratic: I must consume twice, … polynomial: either of these). It does makes sense from a point of view of the mathematical analogy. And Poly means something like “several” in Greek, so it makes sense.
• U: first letter of Unrestricted. Easy to use, but a one-letter name may be consider a bit too rare and precious for this use.
• This: short, but ultimately hard to convey an intuition. It sounds a bit like it ought to mean the identity, which I don't think is a very good intuition. It could work if we have a story for how this makes sense. It does have the advantage that it comes with a reasonable name for X: s `AndThis` a.
• Lax: mostly a synonymous of Unrestricted. But nobody's really convinced by it
• Freely, Surely: adverbs in the tradition of using such adverbs to pronounce modality (sometime !a is pronounced “certainly a”, see also “there merely exists” in homotopy type theory).
  • It could be a corresponding adjective, though Free is already taken, and Sure sounds weird. (like is “p is a mere proposition”)
  • Or an adverb of the same kind as Maybe
• Box: very generic
• With: this one has a bit of a twist, we would have

  type With :: Multiplicity -> Type -> Type
  data With p a where
    With :: a #p-> With p a

  So that With 'Many a is Unrestricted a. But since this last case is so common we would make a shorthand, such as With'.
• More: A bit like Many. Though it may sound a bit excessive, I guess.

I am, personally, fully convinced by none of these. But they are good starting points. Naming is hard. But, sometimes, after stumbling in the dark for a while, we suddenly fine the name which should have been obvious all along. Help me find it.

Merge (via git-subtree-ing) an optimized, documented version of linear-streams (with sufficient workarounds for the API that can't be implemented properly without affine streams, e.g., readStdinUntil :: (String -> Bool) -> Stream (Of String) IO ()).

Currently, data functors and control functors have type

fmap :: (a ->. b) -> f a ->. f b

and

fmap :: (a ->. b) ->. f a ->. f b

respectively. (that is data functors are regular functors and control functors are enriched functors).

But with polymorphism, it seem that we may want to split them further. Based more on how they are used (data functors are data containers of sorts, which control functors are effect-bearing computations).

My thoughts are the following: just like for lists the type of data functor's fmap would become

fmap :: (a # p -> b) -> f a # p -> f b

(it specialises to linear data functor when p ~ One and to regular (unrestricted) functor when p ~ Omega). It is not equivalent, but it seems to make sense. The only downside, though, is that it may be a bit weird for types which are always linear in the context (like a pure mutable array, for instance). An alternative is to do:

class Functor (p :: Multiplicity) f where
  fmap :: (a # p -> b) -> f a # p -> f b

This way we have polymorphism without the weirdness.

On the other hand, for control functors, we care about linearity of the control, but not linearity of the data. Therefore, we can the multiplicity of the data variable, like IO in the paper.

class Functor (f :: Multiplicity -> * -> *) where
  fmap :: (a ->. b) ->. f p a ->. f p b

(maybe a variant of type (a # p ->. b) ->. f q a ->. f (p * q)? Really the general form would be (a #p ->. Mult q b) ->. f p a ->. f q b).

The bottom-line is that control functors become functors from the category where objects are pairs (a, p) of an object and a type, and maps from (a, p) to (b, q) are a # p ->. Mult q b, to the category of types and linear functions (enriched in the category of types and linear functions).

This is not a restriction because you can always compose your old-style control functor with Mult p to obtain a new one. It also extends to a notion of monad (more precisely, of relative monad).

Which is the whole point of the change: it will make do notation much more pleasant, with the ability to return linear or unrestricted values.

In linear-base, we took the decision of making Optic a newtype to improve on the error messages from the lens library. (While retaining the same spirit of subtyping-by-typeclass-subsumption. So not quite the same level of control as what the optics library aims for. Some kind of middle ground.)

A consequence is that we can't use the (.) as a lens composition operators: lenses are not functions. They do not even form a category, at least not naturally (you can form a category of optics where the objects are pairs of types, but we would have to make it apparent in the Optic types, which would have to take two pairs of types as arguments instead of 4 arguments, and we would need a general enough definition of category to make that stick. It's not strictly impossible but it's beyond the scope of linear-base).

We've been using the symbol (.>) for composition (my intuition was some sort of a mix between the . notation for records and the F♯/Ocaml pipe operator (|>) denoting sequence). But in the lens library, this particular symbol is also used, to mean the composition of a regular lens (to the left) with an indexed lens (to the right). So maybe using (.>) doesn't follow the principle of least surprise.

So this issue is to try and figure a better operator for optic (lens, prisms, traversals, …) composition.

Is your feature request related to a problem? Please describe.
There is no way currently to use optics without importing an internal module. There is a Control.Optics.Linear.Internal module but no Control.Optics.Linear.

Describe the solution you'd like
Add a Control.Optics.Linear module. If it's fine to export everything from Control.Optics.Linear.Internal, then just rename that one.

Currently, the only way to construct a (non-constant) Push Array is via a Pull Array. This is undesirable if the elements cannot be conveniently given in an arbitrary order, as a Pull Array demands. Similarly, the intuition for Push Arrays is that they should be friendly to construct, but this is not reflected in the API.

Currently, most of our linear collections (Array, Vector.Mutable and HashMap) take the collection as a first argument. Here are some examples from linear base:

Data.Array.Mutable.Linear.write :: HasCallStack => Array a #-> Int -> a -> Array a
Data.Vector.Mutable.Linear.write :: HasCallStack => Vector a #-> Int -> a -> Vector a

This is also what vector library does.

But there are also places where we do the opposite:

Data.Array.Mutable.Linear.resize :: HasCallStack => Int -> Array a #-> Array a
Data.Array.Polarized.Pull.foldr :: (a #-> b #-> b) -> b #-> Array a #-> b
Data.Array.Destination.split :: Int -> DArray a #-> (DArray a, DArray a)

(Also, as expected, the functions we re-implemented from base also tend to take the collection as the last argument)

I think, taking the collection as the last parameter has some benefits:

• I believe most libraries are using the collection-last argument order.
• It makes point-free usage nicer (vec & write 0 'a' & write 1 'c')
• Usually our functions are linear on the collection, and not on the rest. So, a type signature like:

write :: Int -> a -> Array a #-> Array a

Makes it clear that "given an Int and an a that we're linearly transforming an Array to another". The alternative:

write :: Array a #-> Int -> a -> Array a

In my opinion does not read as well, the unrestricted arrow before the result gives me the wrong impression.

The disadvantages I can think of:

• Differing from the vector library.
• We have to change some amount of code.

No matter which order we choose, it would be good to stick to it across the codebase.

This issue is broken up from the original PR: #146

The test suite (examples) is currently deactivated due to a linearity bug. I have no idea what is happening and had no time to investigate yet. It seems to be a bad interaction with hspec which would be rather high priority.

I've followed the steps from the readme in a new project, and I get the following error:

02:12 PM noon ∈ linear-types stack build
Stack has not been tested with GHC versions above 8.10, and using 8.11, this may fail
Stack has not been tested with Cabal versions above 3.2, but version 3.3.0.0 was found, this may fail
WARNING: Ignoring vector's bounds on base (>=4.5 && <4.15); using base-4.15.0.0.
Reason: allow-newer enabled.
WARNING: Ignoring primitive's bounds on base (>=4.5 && <4.15); using base-4.15.0.0.
Reason: allow-newer enabled.
primitive      > configure
primitive      > Configuring primitive-0.7.0.0...
primitive      > build
primitive      > Preprocessing library for primitive-0.7.0.0..
primitive      > Building library for primitive-0.7.0.0..
primitive      > [ 1 of 13] Compiling Control.Monad.Primitive
primitive      > 
primitive      > /run/user/1000/stack-fc9f49f9c873bb1e/primitive-0.7.0.0/Control/Monad/Primitive.hs:27:21: error:
primitive      >     Module ‘GHC.Base’ does not export ‘unsafeCoerce#’
primitive      >    |
primitive      > 27 | import GHC.Base   ( unsafeCoerce#, realWorld# )
primitive      >    |                     ^^^^^^^^^^^^^
            
--  While building package primitive-0.7.0.0 using:
      /home/noon/.stack/setup-exe-cache/x86_64-linux-nix/Cabal-simple_mPHDZzAJ_3.3.0.0_ghc-8.11.20200630 --builddir=.stack-work/dist/x86_64-linux-nix/Cabal-3.3.0.0 build --ghc-options " -fdiagnostics-color=always"
    Process exited with code: ExitFailure 1
Progress 1/4

To Reproduce

1. Start a new project with stack new linear-types --bare simple-hpack
2. Follow the README - https://github.com/tweag/linear-base#getting-started
3. Build with stack build

Expected behavior

The build to work!

Environment

• OS name + version: Linux 4.15.0-109-generic #110-Ubuntu SMP Tue Jun 23 02:39:32 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux
• Version of the code: Tried with the revision in the readme, as well as 705522f0bad3f1083bb3447b9f476f6f84d21410

Is your feature request related to a problem? Please describe.
It's unclear that module in linear-base should typically depend on Prelude.Linear.Internal, which is one of the very first modules in the dependency hierarchy, while Prelude.Linear is allowed to be very late. See the discussion in #138 .

Describe the solution you'd like
This could be documented in the README or any file describing the module architecture. In addition, there ought to be a description of these module roles in their Haddock header.

#The type of bind in the RIO and Linear monads ought to be polymorphic.

This is an instance of #27.

For instance, we should have the following:

(>>=) :: RIO p a #-> (a ->.(p) RIO p' b) #-> RIO p' b

We currently have (in System.IO.Linear and System.IO.Resource) the following:

(>>=) :: RIO a #-> (a #-> RIO b) #-> RIO b
(>>) :: RIO () #-> (RIO b) #-> RIO b

In order to use do-notation with -XRebindableSyntax with linear IO (which came up when writing linear-streams), the linear IO monad needs a regular Prelude monad instance.

Data.Array.Mutable.Linear module comes with these functions:

-- | Using first element as seed, resize to a constant array
resize :: HasCallStack => Int -> Array a #-> Array a
resize newSize (Array _ mutArr) =
  let !(# a #) = Unsafe.readMutArr mutArr 0
  in  Array newSize (Unsafe.newMutArr newSize a)

-- | Resize to a new constant array given a seed value
resizeSeed :: HasCallStack => Int -> a -> Array a #-> Array a
resizeSeed newSize seed (Array _ _) =
  Array newSize (Unsafe.newMutArr newSize seed)

I find them counter-intutive, since I don't expect a resize operation to lose most/all of the elements unless we are shrinking the array. I suggest we replace them with growBy and shrinkTo functions:

-- | Grows the array by given number of elements, using a default value.
growBy :: HasCallStack => Int -> a -> Array a #-> Array a

-- | Shrinks the array to contain given number of elements.
shrinkTo :: HasCallStack => Int -> Array a #-> Array a

We can also provide a resize function can do both. Also; since these functions almost always copy the array, we can modify the signatures to return the original array too.

It seems like on the codebase resizeSeed function is used for allocating a new array using another array, without requiring a continuation. I think it is better done explicitly with a new alloc variant, something like:

-- | Allocate a constant array given a size and an initial value,
-- using another array as a uniqueness proof.
allocBeside :: Int -> a -> Array b #-> (Array b, Array a)
allocBeside size val orig = (orig, Array (Unsafe.newMutArr size val))

I think above is safe. Let me know if it isn't.

This issue is broken up from: #146

There are a few functions that cannot yet be migrated because we need support from linear-base. Here is the specific list of features needed from linear base and the streaming functions that use them. The task of this issue is to implement these functions when the support becomes available (and perhaps to make these issues in linear-base and build them out).

Things needed from linear base

• Foldable class
• MFunctor class

The things that require them

• each :: (Monad m, Foldable f) => f a -> Stream (Of a) m ()
• concat :: (Monad m, Foldable f) => Stream (Of (f a)) m r -> Stream (Of a) m r
• delay :: MonadIO m => Double -> Stream (Of a) m r -> Stream (Of a) m r (not sure what I need from linear base yet)
• distribute :: (Control.Monad m, Control.Functor f, Control.MonadTrans t, MFunctor t, Monad (t (Stream f m))) => Stream f (t m) r -> t (Stream f m) r

See what's missing from the specification from #161 in the current setup of optics and implement it.

• Make the HashMap tests as elegant as the Data.Array.Mutable.Linear tests. That is, use === from hedgehog and have the allocation functions take HashMap k v #-> Unrestricted (TestT IO ()). Also, have as systematic an approach to testing. (There are currently too few tests.)
• Rename the list generators non_empty_list and so on. Make sure that anything that can be tested with empty lists is. In general, make sure the domain, the X in "forall a in X. axiom(a)" is fully covered.

Right now, mutable vectors and mutable arrays both use Unsafe.MutableArray. Most of what Vector does repeats code from mutable arrays.

This should be fixed, probably by implementing mutable vectors in terms of mutable arrays, or just by having one array type with the functionality of both.

In the lookup of a hashmap and similar cases, we have a common pattern of wanting something like one of the following options. Which one should we choose?

• Maybe (Unrestricted a)
• Unrestricted (Maybe a)
• data MaybeU a where MaybeU :: a -> MaybeU a

Figure the following out:

• Should Num be a superclass of Prelude.Ord? or Ord.Linear?
• How about Eq?
• In general, what is the relationship between ordering and numeric types that we should encode?

I've used Storable as a shortcut to implement off-heap data. But this is incorrect on two accounts:

• Storable assumes that it has unrestricted argument (in particular for poke), whereas we most often have linear values to pass to poke.
• Storable is in IO, which is too unconstrained for our use-case. In principle, peek or poke could have effects which escape the unsafePerformIO call.

I don't have a good solution a replacement type class yet. I'll use this issue to track my thoughts.

I haven't examined this closely, but we might want linear versions of what's re-exported in Data.Semigroup.

Describe the bug

As a result of #135, Data.Array.Mutable.Linear.Array is stricter than necessary; read's force the elements to WHNF. This is counter-intutitive since most other Haskell collections are lazy on the values.

To Reproduce

{-# LANGUAGE LinearTypes #-}
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module Main where

import Data.Function ((&))
import qualified Prelude.Linear as L
import qualified Data.Array.Mutable.Linear as Array
import Prelude.Linear (Unrestricted(..))

processArr :: Array.Array () #-> Unrestricted ()
processArr arr =
  Array.write arr 0 (error "this should not be evaluated") L.& \arr ->
  Array.read arr 0 L.& \(arr, Unrestricted _) ->
    arr `L.lseq` Unrestricted ()

main :: IO ()
main =
   Array.fromList [()] processArr
     & \(Unrestricted a) -> print a

Expected behavior

We expect the above program to print (), however it currently fails.

We should also have a test case for this.

With the release of GHC 9.0, which will feature linear types, approaching; we are also preparing a release of linear-base.

And in order for this to happen, it is time to pay attention to some things which we had so far neglected. That is, stuff scoring high in the Wadler's law scale. By virtue of them taking time, we have consistently put off thinking about naming too much, and ploughed forward with temporary names for many things, so that we could make progress on implementation.

But now is the time. We have the bikeshedding label to group these issues. So if you are into this sort of things, join us there and contribute your opinion.

Currently, our mutable Vector, Array and HashMap constructors are of this form:

alloc :: ... -> (Thing a #-> Unrestricted b) -> Unrestricted b

This is too general specific; since it doesn't mention that the continuation will only be used once, we can not use a linear value from the outer scope inside the continuation. Consider this example:

data Thing = Thing
instance Consumable Thing where consume Thing = ()

withThing :: (Thing #-> Unrestricted b) -> Unrestricted b
withThing f = f Thing

doSomething :: Unrestricted Int
doSomething =
  withThing (\t1 ->
    withThing (\t2 ->
      t1 `lseq` t2 `lseq` Unrestricted 42
    )
  )

This does not compile, since t1 is used inside the inner continuation, however the result of the inner withThing does not guarantee that it'll use the computation once.

To fix this, we should replace them with the form:

alloc :: ... -> (Thing a #-> Unrestricted b) #-> Unrestricted b

As of right now, calling stack ghci will panic when loading Data.Unsafe.MutableArray. It appears to be a regression related to runRW#.

The following code works in current ghci, and panics in the ghci version which is pinned in linear-base nix-shell:

> :set -XMagicHash
> import GHC.Exts
> runRW# $ \s -> 0

As long as this bug persists, we can't use ghcid with linear-base, which is rather no bueno. (though I'm not sure it's the only hurdle for this particular race, currently)

This is probably upstream's 18397. It's being fixed. So this is a reminder to track said issue, and update our head as soon as the bug is fixed.

Currently, our linear mutable Array and Vector implementations require the collection to always contain at least one element inside.

Especially when using a Vector, it is common to start with an empty vector and append new elements to it. Having it require an element to start with is unusual, so we should support having zero elements inside (this includes resizing to zero elements) and provide an empty method.

I think this choice stems from Unsafe.MutableArray.newMutArr's precondition that the size should be positive. However, I did a few quick tests and it seems to be happy when the size is 0 too. So we can probably relax that requirement and the Vector and Array changes would follow.

This issue is broken up from: #146

We redefined Kleisli for the sake of lenses. Considering that it is essentially used internally, it didn't matter, if it would spare a dependency.

However, as it happens, Kleisli is defined in `base. So we should use that one instead (or non-linear Kleisli, of course, the linear has to stay).

I'm excited to use linear types to make sure that my handles are never left open.

It looks like a real pain though to have to manually thread a handle in and out of operations in which it is used ((Handle #-> RIO (Unrestricted Text, Handle) for example)

The type signature h #-> m (a, h) looks a lot like a state monad. Is it possible to abstract over this pattern? If so, would it be possible to add an example of this to this repo?

Currently, Data.Vector.Mutable.Linear and Data.Vector.Mutable.Array have separate, but similar implementations. We can remove some duplication via implementing the Vector in terms of Array.

• Arrays should be ordinary arrays with read and write functions working with indexes and with an explicit resize functionality.
• Vectors should growable arrays supporting push and pop operations efficiently by maintaining some spare capacity.

In testing this out, I (Divesh) found that Prelude.Linear exports Prelude hiding the non-linear ($) and other related tools. This causes problems for most linear apps that have linear and non-linear code.

Maybe it should re-export all of prelude qualified as NotLinear or something. I'll think about it.

For simple things, using forget works, but this gets cumbersome for say ($) and doesn't work for HOFs.

Array TODOs:

--   - Add more of the API from Data.Vector
--   - Remove the use of error on indicies out of bound.

Hashmap TODOs:

--   * Make everything linear, I don't need to use Unsafe.toLinear
--   * Add singletonWithSize
--   * swapFromRead repeats the probe sequence on the recurive insert call
--     and this could be done away with
--   * We don't resize to make the array smaller when we have too much space
--   * Make the lookup use smart search by probing from the mean PSL:
--     probe at the mean, mean-1, mean+1, mean-2, mean+2, ...
--   * Other functions from Data.Map

Vector TODOs:

--   * Is this fast?
--   * Add doc.
--   * Add more of the core API from Data.Vector
--   * Add control instances
--   * Dupable instance
--   * See if you can index by length nicely

In the past, I'd edited traverse to have type signature

  traverse :: Data.Applicative f => (a ->. f b) -> t a ->. f (t b)

(and similar for sequence) - it now seems this was misguided, since it prevents Const, ((,) a), Either e from being Traversable. (And these last two instances are why Strong (,) () and Strong Either Void are superclasses of Wandering). Instead, the correct signature probably ought to be

  traverse :: Control.Applicative f => (a ->. f b) -> t a ->. f (t b)

This change should not prevent any instance from still working, but might need some definitions to be edited.

We have a some typeclasses which is only useful with linear types, namely Consumable, Dupable or Movable. Hence, when writing multiplicity polymorphic functions, we should only require those constraints when the values are used linearly; otherwise non-linear use suffers from unnecessary constraints.

Describe the solution you'd like

I suggest we add wrapper typeclasses with an extra multiplicity parameter; implement a catch-all instance when multiplicity is Many, and refer to the original typeclass when multiplicity is One. Example:

class Consumable' r a where
  consume' :: FUN r a ()

instance Consumable' Many a where
  consume' _ = ()

instance Consumable a => Consumable' One a where
  consume' = consume

lseq' :: Consumable' r a => FUN r a (FUN r b b)
lseq' a b = seqUnit (consume' a) b

Using these, we can easily implement multiplicity polymorphic functions:

lefts :: Consumable' r b => FUN r [Either a b] [a]
lefts [] = []
lefts (Left a : xs) = a : lefts xs
lefts (Right b : xs) = lseq' b (lefts xs)

Which means that I can write multiplicity-polymorphic functions where they only require a Consumable constraint when used with One.

Describe alternatives you've considered

• Instead of adding a new set of classes, we can simply add the additional parameter to existing classes. Then we can also provide a type alias replicating the current kinds. I don't have a preference between this and the solution above.
• We can bikeshed the names.

Roadmap (roughly in order)

• Organizational changes to clean things up
• Build out variants of the fundamentals from base along with a test
  suite:
  • Control
    • Applicative
    • Monad
  • Data
    • Bifunctor
    • Bits
    • Bool
    • Char
    • Either
    • Eq
    • Fixed
    • Foldable
    • Functor
    • Int (done via Num)
    • List
    • Maybe
    • Ord
    • Monoid
    • Ratio
    • Proxy
    • Semigroup (done via Num)
    • String
    • Tuple
  • Numeric.Natural
  • Prelude (almost done)
• Build out and clean up mutable data structures. Aim to make them fast. Have elegant property tests.
• Consider, document and possibly improve the design of
  • Push and pull arrays
  • The whole lens story
  • The non-GC-heap allocation
  • Linear IO
• Examples
  • A mutate-record kind of interface where you can mutate a copy of an object in some closed context. See the Env application in the basecamp post.
  • Another practical real world example. Investigate the list here. Some top contenders: ixy-languages, allocation free Haskell.
• The backlog

Backlog

• Other open issues
• When multiplicity is supported, anything that can be made polymorphic should
  be made polymorphic -- this will make things much more sane.
• There are a lot of old branches that need to be reviewed.

Checklist for Release

• A built haddock page (maybe a github page) with linear arrows rendered properly
• Tutorials

Currently deactivated because of a linearity bug. (I suspect it's due to the fact that workers for a binary data constructor currently uses the same multiplicity for both fields, hence an issue in the linear ghc branch).

It seems like

func :: Maybe Int
func = do
  someDiscarded :: RIO ()
  return (Nothing)
  where
    Control.Builder {..} = Control.monadBuilder

doesn't work.

Check if this truly is the case and if so, fix it.

This issue is to create a very short (< 500 lines) design document specifying what exactly we expect to be able to do with linear lenses at the level of an API. From this document it should be crystal clear whether an implementation meets the specification put forth here.

Currently, the CI uses version 1.0.0 of the tweag/linear-types image, but there are some recent changes it would be worthwhile to test.

Once tweag/ghc#392 is resolved, the CI should be updated to use this new image.

There are some reasonably large modules with very little documentation, such as Control.Optics.Linear.Internal and some with outdated documentation such as Data.Unrestricted.Linear, and thanks to recent module shuffling, some redundant pragmas.
Also, modules such as Control.Optics.Linear.Internal do not need the .Internal suffix currently.

Is your feature request related to a problem? Please describe.
The only way to create a HashMap is singleton, but it's awkward to use because in many settings you don't have the first value to initially populate your HashMap with. E.g. often one needs to make a HashMap out of a list, and the list might be empty.

Describe the solution you'd like
Add withEmpty :: Keyed k => (HashMap k v #-> Unrestricted b) -> Unrestricted b. with in the name of the function is chosen to make it obvious to the reader that withEmpty expects a modifier. E.g. withEmpty (fillFromList xs >>> runAlgorithm) as opposed to empty (fillFromList xs >>> runAlgorithm). Similarly singleton should be renamed to withSingleton.

Describe alternatives you've considered
Dropping singleton altogether. Rejected because it doesn't seem necessary.

Additional context
N/A

Dupable is dual to Semigroup (I have it named Cosemigroup in an experiment I'm working on), and Consumable is dual to Monoid. But the superclass relationship is reversed in this library. Is there a fundamental reason for this? I have a hard time seeing which way it should actually be.

Currently Dupable typeclass requires implementing the dupV function:

class Consumable a => Dupable a where
  dupV :: KnownNat n => a #-> V n a

However, to me, it's not obvious how that can be implemented; and after spending hours on it today I couldn't figure it out. However

dup2 :: Dupable a => a #-> (a, a)

function is simpler to implement, and I think we should define Dupable in terms of this. Dupable's laws are already defined in terms of dup2 instead of dupV, which also points to dup2 being the simpler option.

I had this issue when trying to implement a Dupable instance for Data.Array.Mutable.Linear. The existing Dupable implementations all have simple implementations implemented using V's applicative instance (or using other Dupable instances), but we can not use that if we can not share the value. In Array's case, it's easy to implement a function like clone :: Array a #-> (Array a, Array a), but going from that to dupV was not easy (for me).

We should still keep dupV in the class and define {-# MINIMAL dup2 | dupV #-}, in case when dupV is more efficient.

Some of the Data.Array.Polarized functions allocate unnecessarily, such as replicate and fromFunction in Destination.hs, which means that functions like transfer and walk also have unnecessary allocation.

These should be modified to have no allocation, since the idea of Polarised arrays is that allocations should be explicit.

[because alliterative titles are always the best titles]

Edit: I now have a better solution outlined in #130 (comment)

This is something which has been at the back of my mind for a while. And I'm not exactly sure how to approach it.

Here is the problem: when creating some piece of data which needs to be unique (either for resource handling of or mutation or what have you) there are actually many ways to create such a piece of data.

In linear-base, we use two different ones:

• Delimit the data in a scope withThingy :: (Thingy #-> Unrestricted a) #-> Unrestricted a
• Use a specific control monad newThingy :: M Thingy
  • In this latter case, there are some restriction on the run function of the monad, if the Thingy is to stay unique
  • Typical examples are the IO monad, and its cousin the RIO monad.

These are not completely independent ways to create a unique thingy, since withThingy can be turned into the monadic style with the continuation monad. But they are not the same either, if only because M need not be a continuation monad.

Sometimes one of this styles is required and the other one doesn't really work. But sometimes you may want both. Maybe I can create a linear mutable array with the pure interface, but also with IO. Note how neither is an instance of the other. So I'd basically need two distinct creation functions. Meh…

But, more importantly, there are other ways to create unique thingy. For instance, if I have any guaranteed unique piece of data, I can create a new linear mutable array, and it will remain unique. And so there starts to be a bit of an n*m problem here. Where each type of unique pieces of data need many creation functions. That's unpleasant, to say the least.

So I've been thinking that data should be able to carry some kind of token establishing that they are unique. I've been calling them Source in my head (we can arrange it so that Source is 0-width data, so that they are mostly free).

The rest is a bit hazy in my head, still. But I imagine something like the following: we have a number of ways to build uniqueness sources

newSource :: IO Source
withSource :: (Source #-> Unrestricted a) #-> Unrestricted a

Moreover sources would be Dupable, I assume (which means that they don't guarantee uniqueness, but I think that it is unavoidable).

Then we would have

fromSource :: Source #-> Thingy

(and maybe withThingy and newThingy as convenient shorthands for the appropriate composition)

To be able to create a thingy out of, say, another thingy, without creating a new scope, we could use the following

produceSource :: Thing #-> (Source, Thingy)

Implementing this is what requires Source to be Dupable (this, and whatever consume or freeze function that we would have on the type, though these only require Consumable).

By convention, unique things would always have at least a fromSource and a produceSource.

Something along these lines anyway. Thoughts, further ideas, counterproposals? I want them all!