Is there a notion of lens-to-something-unrestricted?

[aspiwack]

Consider:

data T a b where
  MkT :: a #-> b -> MkT a b

(what matters here is that the second field is unrestricted)

If I have a lens l2 into the second field, then I can actually set the value at l2 linearly (currently, set l2 :: b' -> T a b -> T b', no linearity anywhere).

In #79 , there was

set'' :: Optic_ (NonLinear.Kleisli (Control.Reader b)) a b s t -> b #-> s -> t
set'' (Optical l) b s = Control.runReader (NonLinear.runKleisli (l (NonLinear.Kleisli (const (Control.reader id)))) s) b

to this specific effect.

Unrestricted lenses

But what is the type of l2? Certainly it's not going to be Optic_ (NonLinear.Kleisli (Control.Reader b)), it doesn't compose with anything. A reasonable requirement for the type of l2 is that it is a super type of Lens.

We can probably work this out. In a sense T is the prototypical example. An unrestricted-field-lens should define an isomorphism between a type, and T x b for some x. We basically need a variant of

second :: a `arr` b -> (c,a) `arr` (c, b)

Replacing (,) with T (or something equivalent).

Something to this effect anyway. Maybe we can see it as two properties, one relating to the pair, and one to the unrestrictedness. So that we could deal with unrestricted fields in prisms and traversals as well.

Replace set?

What I'm sort of wondering too, is whether this set'' could subsume set some way. Probably not, to be honest. Though it's a bit sad to have two different set functions which do the same thing, just in slightly different circumstances.

[utdemir]

+1, it seems like this situation is becoming pretty common. I had this issue before while writing lenses for mutable collections, where the collection itself is linear but the elements inside are unrestricted. So I had ended up using something like:

lensAt :: Int -> Lens' (Unrestricted a) (Rec b)

[aspiwack]

I'm on this.

I know how to fix. But, of course, it duplicates every Optics type. In my head, I'm suffixing them with a U, so we would have

type IsoU
type IsoU'
type LensU
type LensU'
type PrismU
type PrismU'
type TraversalU
type TraversalU'

Do we like this? (cc @mboes , if you have an opinion)

[aspiwack]

I actually failed to solve this, today. But I can't yet put intelligible words on it, I'll get back here soon.

[aspiwack]

I think I can put some intelligible words on it, after all. Though it's not the whole story. So, here goes:

The general method for deriving profunctor optics presented in All you need to know about Yoneda §4.5 only works for families of functors which contain the identity function. Here we need the family consisting only of Unrestricted, which doesn't contain the identity.

I'll think about it some more.

[aspiwack]

A little bit of maths (in a Haskelly style) to expand on the previous comment.

The general in the All you need to know about Yoneda paper is the
following.

Existential optics

First, model your lens thing in existential form

type O s t a b = exists f. C f => (s -> f a, f b -> t)

Where C is a type class with the following properties

• C f ⊢ Functor f (that is, typically, C is declared as class Functor f => C f).
• C Identity holds
• (C f, C g) => C (Compose f g)

There is always a natural presentation of an optic under this form.

• Isos take C to contain just the identity functor
• Lenses take C to contain all functors of the form (c,)
• Prisms take C to contain all functors of the form Either c
• Traversals take C to be Traversable

(proofs that these class contain the identity and composition functors
(up to natural isomorphism) are left as an exercise)

Profunctor optics

Now, this form makes it reasonably clear what is happening, but optics
in this form don't compose super well.

So the paper gives a general recipe to transform them into a
profunctor-optic form.

Consider the following class

class Profunctor p => Shaped (c :: (* -> *) -> constraint) p where
  lift :: forall f. c f => p a b -> p (f a) (f b)

Then, O above is equivalent to

type O' s t a b = forall p. Shaped C p => p a b -> p s t

Proof of equivalence

One direction is fairly straightforward.

O2O' :: O s t a b -> O' s t a b
O2O' :: (C f, Shaped C p) => (s -> f a, f b -> t) -> p a b -> p s t
O2O' (focus, rebuild) k = dimap focus rebuild (lift k)

The other direction requires me to prove two lemmas (the Haskell below
is very pseudo)

instance Profunctor (O _ _ a b) where
  dimap :: (s' -> s) -> (t -> t') -> exists f. (s -> f a, f b -> t) -> exists h. (s' -> h a, h b -> t')
  dimap :: (s' -> s) -> (t -> t') -> (s -> f a, f b -> t) -> (s' -> f a, f b -> t')
  
  dimap :: (s' -> s) -> (t -> t') -> (s -> f a, f b -> t) -> (s' -> f a, f b -> t')
  dimap f g (focus, rebuild) = (f . focus, rebuild . g)
  
instance Shaped C (O _ _ a b) where
  lift :: (exists f. (s -> f a, f b -> t)) -> exists h. (g s -> h a, h b -> g t)
  -- This uses that `C` is stable by composition
  lift :: (s -> f a, f b -> t) -> (g s -> Compose g f a, Compose g f b -> g t)
  lift (focus, rebuild) = ((\gs -> focus <$> gs), (\gfb -> rebuild <$> gfs))

Now, what's left is:

O'2O :: O' s t a b -> O s t a b
-- This uses that `C Identity` holds
O'2O :: (p ~ Shaped C (O _ _ a b)) => (p a b -> p s t) -> (s -> Identity a, Identity b -> t)
O'2O o = o (Indentity, runIdentity)

Unrestricted

Now, let's get back to this unrestricted business. The simplest optic
to unrestricted is IsoU, which, in existential form looks like

IsoU = (s %1-> Ur a, Ur b %1-> t)

But, as I was saying in the comment above, Ur is not
equivalent to Identity (it is, however, equivalent to Ur ∘ Ur). Therefore, this form is not equivalent to

class Profunctor p => Unrestricting p where
  unrestrict :: p a b -> p (Ur a) (Ur b)
  
IsoU = forall p. Unrestricting p => p a b -> p s t

(or, if it is, the proof doesn't follow from the generic proof
above. But if I had to bet, I'd say that they aren't equivalent)

Case in point, I haven't been able, from the profunctor definition
above, to define the quintessential optic-to-unrestricted function:

overU :: IsoU s t a b -> (a -> b) -> s %1-> t

Until we have functions in this style, we basically can't use an
optic-to-unrestricted.

The reason, by the way, why all of this matters right now, is that our
mutable arrays and hashmaps all contain unrestricted things. So
indexing in them need to be traversals-to-unrestricted.

[aspiwack]

In a Twitter conversation with Edward Kmett, the other days. I realised that there were some commonalities between his search for a way to compose regular optics with optics on indexed type, and this here issue whereby we want optics to either linear and unrestricted parts.

It's probably not going to align quite exactly, but maybe there is something to glean from his exploration. The current state of which can be found in this gist.

[Divesh-Otwani]

I haven't combed through the math yet, but I agree that we need something that works on unrestricted fields. The existential formulations with T x a seem messy but that's just my instinct right now. I don't know if we can generalize a linear Lens but it would be great if we didn't have versions of optic functions postfixed with U. We don't need linear isomorphisms or prisms. This is really about changes we want to linear lenses and traversals.

I'll circle back to this when I tackle optics 😉

[Tarmean]

I played with linear Van Laarhoven lenses to explore the design space a bit. The basics seem fairly nice but I haven't quite figured out how to avoid allocating when getting unrestricted data stored in restricted structures.

A basic lens has linear arrows everywhere. This is necessary if we want to use a lens to swap a linear value with another one.

type LLens f s t a b = LFunctor f => (a %1 -> f b) %1-> s %1-> f t

LFunctor is a Functor variant that also has linear arrows everywhere, e.g. f a contains exactly one a.

 fmap1 :: LFunctor f => (a %1 -> b) %1-> f a %1-> f b

_2 :: LFunctor f => (a %1-> f b) %1-> (x,a) %1-> f (x, b)
_2 p (l,r)= fmap1 (\o -> (l, o)) (p r)

A very useful interface is this replace function:

replace :: LLens (Replace x) s t a b %1-> (a %1->(x, b)) %1-> s %1-> (x, t)

It can get linear values by copying with replace l dup, extract a value from a linear map by replacing with something empty, swap two values, etc. Replace is a named tuple type.

Traversals can use L.Applicative and also lose the linear arrow on the inner lens. Replace has to hold a linear Monoid, pretty much like Const.

type LTraversal f s t a b = (a %1 -> f b) -> s %1-> f t

mapped :: (L.Applicative f) => (a %1-> f b) -> [a] %1-> f [b]
mapped f (x:xs) = (:) L.<$> f x L.<*> mapped f xs
mapped _ [] = L.pure []

These arrows have different multiplicities so composing lenses with traversals requires multiplicity polymorphic function composition. Couldn't get that to typecheck without unsafe coerce:

(%) :: (b %x-> c) %1-> (a %y->b) %x-> a %(MultMul y x)-> c
(%) =  unsafeCoerce (.)

test :: (PL.Adding Int, [(String, ())])
test = foldBy (mapped % _2) (\a -> (PL.Adding a, ())) [("foo", 1),("bar", 2),("baz", 3)]
-- (PL.Adding 6, [("foo", ()),("bar", ()),("baz", ())])

For unrestricted bits we can drop even more linearity, allowing us to use standard lens lenses! I feel like there should be a way to avoid copying when getting/aggregating with this type?

ur :: Functor f => (a -> f b) -> Ur a %1-> f (Ur b)
ur f (Ur a) = fmap Ur (f a)
type UrLens f s t a b = (a -> f b) -> s %1-> f t

My main issues with this approach is that getting with replace is pretty inefficient. It hopefully is possible with an UrLens but I haven't yet figured out how to make the unrestricted parts efficient but the restricted parts safe. Maybe it requires two functors and the ur lens swaps from Const to Replace?

[Tarmean]

After playing some more, I'm pretty sure fully efficient lenses for nested mutable data require borrowing.

Immutable borrows are like constant time freezing, possibly with scope. Problem is that no mutable data may be reachable from the NonMut version so if any type gets the class instance wrong there are annoying bugs. Compiler support or at least good generic deriving should help.

type family NonMut s f = d | d -> s f
freeze :: s %1-> NonMut Static s
borrow :: s %1-> (forall x. NonMut x s -> a) %1-> (s, a)

Secondly, briefly turning mutable data into Destination Passing Style. This means:

• A scoped area where the reference only occurs in negative positions
• After the area, the original pointer is still valid

This means some types require an additional step of indirection so that e.g. offset changes or reallocation don't desynch the pointers.
Functions either use a scoped token akin to RealWorld#, or return () and rely on strictness like Data.Array.Destination currently does to define ordering.

write :: Int -> a -> Ref s (Array a) -> Tok s %1-> Tok s
mutBorrow :: s %1 -> (forall x. Ref x s -> Tok x %1 -> Ur o) %1-> (s, o)
unsafeBorrow :: s %1 -> (forall x. Ref x s -> o) %1-> (s, o)

NonMut allows us to use non-linear lenses to get/aggregate cleanly, the unrestricted parts aren't affected by the NonMut type family so we can easily extract them from the existential. The mutBorrow is more finegrained where we only skip a single layer of linear mutability but can mutate nested values.
The skolems are ugly and might be circumventable with existentials, maybe it's possible to put the existential skolem variable in the multiplicity. Haven't thought too much about how this would actually work. Maybe with a many-use multiplicity less than 'Many?

borrow :: s %1-> (forall x. (MultGreater 'One x, MultGreater x 'Many) => NonMut s %x-> Ur a) %1-> (s,a)