Practical results using Vector.Mutable.Linear, State and Lens

[Mansindam]

Here is the use-case:

1. linearly mutate a vector
2. freeze it so some functions can duplicate it and read it
3. when that terminates unfreeze it and continue linear operations

Is there a natural way of doing this? In particular it seems difficult to ensure functions using the duplicated frozen vector terminate before proceeding

[Mansindam]

This seems safe:

withVector :: (V.Vector a -> r) -> LV.Vector a %1 -> (r , LV.Vector a)
withVector f = Unsafe.Linear.toLinear \v -> (,v) $! f (L.unur (LV.freeze v))

I also suggest renaming Vector to Stack, it's a less overloaded and unambiguous

[aspiwack]

I assume you mean that V.Vector is the type from the vector library. If so, it isn't sound. Think of withVector id.

But you could have the “borrowed” vector be Duplicable, rather than merely unrestricted, perhaps? You could setup the borrow as something of the form

temporaryFreeze :: MArray a %1 -> (RArray a %1 -> Ur b) %1 -> (Ur b, MArray a)

Where RArray is the type of your read-only duplicable arrays (where the duplication is really just implemented as pointer sharing). I'm not sure that it'd work terribly well. But it's a start.

[Mansindam]

Unfortunate.. Even vector transformations produce copies, so only variants of identity are leaking duplications
This seems to me at least like a vital primitive

Ultimately these things are boxed though, I will need unboxed versions that can be directly FFI'd for simd (ghc simd doesn't work in repl, which is too irritating)

Similarly I need a 'copyAppend' primitive which does

  v' %= let len = fnSize + 1 in \v0 -> -- LV.growToFit len >>> \v ->
    foldl (L.toLinear2 (\v i -> LV.get i v & \(L.Ur val , w) -> LV.push val w)) v0 [start .. start + len]

But this is orders of magnitudes slower than the grow followed by MV.move (MV.slice dlen len v) (MV.slice start len src) from IOVector

I needed to add vfoldl :: forall b a p. (b %1 -> a %p -> b) -> b %1 -> V.Vector a %p -> b , any reason why foldl is forcibly linear on everything?
probably should work on a Traversable/Foldable

[Mansindam]

Shouldn't size ideally be 0-multiplicity on the vector?
Is that unsupported by ghc atm?

Edit: Probably nonsense, but typing Get at 0-multiplicity could be convenient, although unsafe if laziness allows keeping stale references around

[aspiwack]

I would love size to be 0-multiplicity. It does make sense at some level. But, it's not clear that it's possible. The biggest problem is that it makes inlining dangerous. Compare

  let x = mutate y in
  let n = size x in
  use x

  let n = size (mutate y) in
  use (mutate y)

Does the second mutate y twice? It's really not the intention is it? We also have to be careful about use-after-free issues. So I'm not sure.

It's really not on my immediate list of priorities to figure this out. But I do agree that this sounds sensible in principle.

[Mansindam]

It starts to morph into something slightly different to a linear type; Some sort of resource protocol basically, I guess it's a different kind of %, but still must have access to the linearity mechanism

[Mansindam]

Is it just not possible to use let to bind linear names? mklinearthing & \linear -> _ seems to be the only syntax that works

[aspiwack]

My answer to that is in the linear constraint proposal.

You can do without linear constraint by using some tokens manually.

[Mansindam]

For 'Unique' types, is there a path for inference to reject constructions using non linear arrows on it?
That is potentially a massive pitfall for beginners, especially considering the non-existent error messages they may find out that their entire strategy is wrong after writing 99% of it (eg. when attempting to use libraries that only export existental linear uses on it)

I like the constraint on the arrow but intuitively its mostly the newtype that doesn't want to be misused

[Mansindam]

Some more experiments

In order to get a State containing linear vectors going It seems mandatory (?) to define lens with a passthrough

v          = LLens.lens \(IEnv p t i l f c) -> (p , \(r,x) -> (r , IEnv x t i l f c))
v'         = LLens.lens \(IEnv p t i l f c) -> (p , \x -> IEnv x t i l f c)

-- Now normal stateful lenses can be defined and can call Linear.Vector.size
l %%= f = state (LLens.over l f)
eg = (v %%= LV.size) >>= \(L.Ur sz) -> .. 

Am I missing anything?
If not, the L.Ur quickly becomes irritating; is there any (even theoretical) solution for managing product types at different linearities?
It seems crude to aggressively distribute the linearity eg. (a,b) %1 => both a and b must be %1

[aspiwack]

Sorry, I didn't understand this question.

[Mansindam]

I'm unsure whether the state strategy is a good idea:
Multiple fields have to be wrapped in Ur
Multiple lens have to be defined, one for %= and %%= (Perhaps I misdefined some of these)
There are 3 components to the state: readonly parameters, mutatables and linear mutatables, the 3 do not coexist smoothly

Composing monads (or ideally, datatypes via subtyping within the state monad) is basically non-viable in haskell
The alternative to State monad: returning explicitly the data and a tuple/ special field for passthrough is perhaps more verbose
Although.. maybe that can be smoothed over with the right Lens functions and an explicit return parameter in the state data

At the same time, the monadic style is convenient, and besides I'm trying to port an intricate 600+line program that frequently mutates MVectors in IO ()

[aspiwack]

Welcome! I took the liberty to convert this into a discussion because there's too much going on for an issue.

[Mansindam]

Why does freeze return a Ur ? That seems redundant to me since no API's care about duplicating standard vectors
In fact generally returning Ur seems always pointless

[tbagrel1]

Usually in linear API we have a scope function of the form withLinearity :: (a %1-> Ur b) %1-> Ur b; to prevent the a from escaping and being used non-linearly.

If I have a function foo :: a %1-> Ur b, it signals the b, unlike the a, is allowed to escape the scope of withLinearity and outlive the resource a.

Typically we can imagine a scope function withFile :: (File %1-> Ur b) %1-> Ur b, and a function closeAndCollectStats :: File %1 -> Ur FileStats. Thanks to the Ur in positive (return) position, we can do

let stats = withFile $ \f -> .... `lseq` closeAndCollectStats f

so that FileStats can survive the scope of the file. Ur in return position is a laisser-passer to escape an otherwise linear scope.

[Mansindam]

Again, no

withFile :: (File %1-> Ur b) %1-> b Is safe, it's a proof obligation on the inputs, and meaningless as an output

[tbagrel1]

In fact generally returning Ur seems always pointless

How would you write closeAndCollectStats signature without a Ur and still allow that stats survive the file, and escape from withFile?

withFile :: (File %1-> Ur b) %1-> b Is safe, it's a proof obligation on the inputs, and meaningless as an output

The Ur on withFile might not be very useful here. But let's imagine file accesses are only permitted if the user has a linear token, we would have a call to withFile :: FSToken %1 -> (File %1-> Ur b) %1-> Ur b. Probably FSToken usage is restricted through a form of scope function somewhere in parent scopes. In that case the Ur is useful so that stats can escape through many linear scopes.

You can go from withFile :: (File %1-> Ur b) %1-> Ur b to withFile' :: (File %1-> Ur b) %1-> b easily (just compose with unur: withFile' = unur . withFile), while you can't go from withFile' to withFile (because the scope function File %1-> Ur b may capture linear things, we cannot just do withFile f = Ur (withFile' f)). I don't see why we shouldn't implement the more general version of the two (aka withFile) and derive withFile' from it.

EDIT: I had switched withFile and withFile' in my last sentence. It should be ok now.

[Mansindam]

while you can't go from withFile' to withFile (because the scope function may File %1-> Ur b may capture linear things, so we cannot just do withFile' f = Ur (withFile f)

Complete nonsense

[aspiwack]

@Mansindam I will have to ask you to be respectful. Sentences like “complete nonsense” are very much not welcome.

[Mansindam]

data Next a seed = End seed | Skip seed | Next (L.Ur a) seed
unfoldSeed :: (seed %1 -> Next a seed) -> seed %1 -> (V.Vector a , seed)
unfoldSeed fn s0 = let
  go (stack , step) = case fn step of
    Next (L.Ur v) seedN -> Right (LV.push v stack , seedN)
    Skip s              -> Right (stack , s)
    End s               -> Left ((,s) <$> LV.freeze stack)
  in L.unur $ LV.empty \v0 -> tailRecurse1 go (v0 , s0)

This is already decent, but I want %p on the existential
Unfortunately LV.empty forces %1 on the entire tuple

Our favorite Ur hack doesn't work here as something is lost (probably ghc incompetence with this firstclass polymorphism on the multiplicity)
Generally I'm unsatisfied with the granularity of linearities on components of product types, it requires too much boilerplate

I think I want (a %pa , b %pb) -> _
And possibly some ability to predeclare that for record types used as inputs

[Mansindam]

Remarkable oversight

• No instance for ‘Prelude.Monad (StateT IEnv Prelude.Identity)’
    arising from a do statement
  There are instances for similar types:
    instance [safe] Prelude.Monad m =>
                    Prelude.Monad (Prelude.StateT s m)

[Mansindam]

Are Type applications supposed to work?

• Cannot apply expression of type ‘a0 %1 -> Int -> a0’
  to a visible type argument ‘Word64’
• In the expression: clearBit @Word64 b c

[Mansindam]

This is rough:

empty :: forall a b. (Vector a %1 -> Ur b) %1 -> Ur b

stuff :: LV.Vector a %1 -> LV.Vector b %1 -> (LV.Vector a , LV.Vector b)
stuff = _

ko :: LV.Vector a %1 -> LV.Vector a
ko p = LV.empty \v -> stuff p v &
   \(p2 , v2) -> (p2 , LV.freeze v2) -- We lose here; no way to linearly pass p through this Ur bottleneck

The design with Ur is fundamentally imprecise, We want "The input linear variable dies here", not "all linearity dies here"

[Mansindam]

Well it appears this is known.. silly me for reading this entire repo, finding no mention of the linear-constraints proposal and assuming it was ready