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

aspiwack commented 3 years ago

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 commented 3 years ago

+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 commented 3 years ago

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 commented 3 years ago

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

aspiwack commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 :wink:

Tarmean commented 3 years ago

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 commented 3 years ago

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)

aspiwack commented 11 months ago

I think I've finally got this story mostly figured out. This largely follows from @Tarmean 's thoughts above (except the borrowing part which is a different focus, and I won't be trying to nail properly until the linear constraints are landed).

I didn't know what to do with said story until now (obviously….) because these lens types simply don't compose well. And I didn't know how to achieve similar properties with profunctors.

I was simply too focused on giving the profunctor natural properties. We define Strong in terms of second :: b `arr` c -> (a, b) `arr` (a, c). This makes a lot of sense. But it will often be inefficient, and it's not as flexible as the van Laarhoven definition.

Something that @guaraqe taught me many months ago, but didn't click until now, is that you don't have to define Strong this way. You can define Strong in terms of van Laarhoven lenses:

class Strong arr where
  mk :: (forall f. Control.Functor f => (a %1 -> f b) -> (s %1 -> f t)) -> a `arr` b -> s `arr` c

When we've defined a profunctor property this way, we are in the best of both worlds. We have efficient definitions, all the flexibility of van Laarhoven lenses at our fingertip, and the composability of profunctors. The one downside is that I'll have to renounce defining Strong as parameterised over a monoidal product as each monoidal product is liable to have a different van-Laarhoven style definition of strong.

So, we can just follow @Tarmean and define UStrong for use with lenses-to-something-unrestricted:

class UStrong arr where
  mk :: (forall f. Data.Functor f => (a -> f (Ur b)) -> (s %1 -> f t)
  -- Maybe Base.Functor, but I don't think it's enough. Maybe we can write `b` instead of `Ur b`.
  -- It it was Base.Functor it would clearly be equivalent. I don't think it's the case with Data.Functor

One remaining difficulty will be, then, to figure out the appropriate sub-classing relation. But I think this works.

PS: I don't actually know a van-Laarhoven style definition for prisms. it wouldn't be of the form forall r. C f => (a -> f b) -> (s -> f t). Maybe it could be forall r. C f => (f a -> b) -> (f s -> t). Or maybe there's no hope of doing better than left/right like in the lens library.

aspiwack commented 11 months ago

About subtyping.

A lens-to-unrestricted is not a linear lens: a linear lens lets you replace the initial value with something which contains linear free variables, something you can't do under Ur. Conversely, in a lens-to-unrestricted you can replace x by (x,x), which you can't in a linear lens.

So it seems to me that the two hiearchies are completely independent. I'm not sure either that the approach in my previous message is able to prove that if I use a linear lens inside of a lens-to-unrestricted, then I'm a lens-to-unrestricted. Maybe it's alright. Unfortunate. But an acceptable trade-off.

aspiwack commented 5 months ago

Actually, I think that the definition of UStrong should use Control.Functor:

class UStrong arr where
  mk :: (forall f. Control.Functor f => (a -> f (Ur b)) -> (s %1 -> f t)) -> a `arr` b -> s `arr` t

Because if I have (x, Ur a), and I want to focus on the a, I get (x, f (Ur b))). The ability to do (x, f y) %1 -> f(x,y) is precisely what differentiate Control.Functor from Data.Functor (because in a self-enrichment, strong = enriched).

If I have (x, Ur (y, a)), then the definition lets me focus the a. Because Ur (y, a) is isomorphic to Ur y, Ur a.

Do traversals follow the following definition?

class UWandering arr where
  mk :: (forall f. Control.Applicative f => (a -> f (Ur b)) -> (s %1 -> f t)) -> a `arr` b -> s `arr` t

It looks plausible to me. Simple cases (such as data MmmList x a where { Nil :: List a; Cons :: x %1 -> a -> List a %1 -> List a } seem to be amenable to this definition, I see no reason to think that it wouldn't generalise properly. This ought to work.

In both cases there's a bit of waste due to boxing and unboxing with Ur. This could be addressed, in the long run, with #27 .

Musings:

Returning to this, I find it interesting that this doesn't appear to fit the usual categorical framework (because, as I point out upthread, the family of functors which our profunctor distributes with doesn't contain the identity functor). We have a family of functors that compose, the composition must contain at least one Ur, and the fact that Ur (a, b) is isomorphic to (Ur a, Ur b) seems crucial there (and probably so is the fact that Ur (Either a b) is isomorphic to Either (Ur a) (Ur b)). This is a very peculiar variant, which is probably not mathematically particularly compelling.

If we didn't have this property, we'd have to deal with the fact the focal point may not be in the same category as the whole structure. Which is not such a far fetched situation to be in (what I'm saying, I think, is: not all functors are endo). I'm still curious to understand whether there is a good way to write and compose optics which cross categorical boundaries like this.

sjoerdvisscher commented 5 months ago

For an existential optic it doesn't seem to a big problem if the focal point lives in a different category than the whole structure. I.e. if s and t live in c, a and b live in d, and we have some functor (*) :: e -> d -> c then exists (m :: e). (c s (m * a), c (m * b) t) would do the trick.

aspiwack commented 5 months ago

Indeed! But the usual framework requires e to be a monoidal category, and (*) to map tensor product to composition and tensor unit to identity (both of which only make sense if d = c). This really makes me think of the relative monad story where the identity functor is replaced by an arbitrary functor. Here we want the (*) to be monoidal “relative to Ur” whatever that means. This is, I believe, the missing bit, from a sheer maths perspective.

sjoerdvisscher commented 5 months ago

So that would be a skew-monoidal category? Then the tensor unit maps to Ur and the tensor product of m and n maps to Compose (Lan Ur (m *)) (n *). Where I think Lan has to have all arrows linear:

data Lan g h a where
  Lan :: (g b %1 -> a) %1 -> h b %1 -> Lan g h a

I.e. Lan Ur lifts a functor from Hask -> Linear to Linear -> Linear.

aspiwack commented 5 months ago

I'll need to understand it better, but I think you may be right! Thanks a bunch!

@bobatkey would you believe it? After all these years I may be converted to skew-monoidal gadgets :smile: .

BartoszMilewski commented 5 months ago

I think linear types and linear lenses could be modeled using bicategories.

The non-linear case is a 1-object bicategory and a pseudo-functor that maps it to Cat. We have:

0-cell -> monoidal category C
1-cells -> objects in C
composition -> tensor product
2-cells -> morphisms in C

To model linear types, we need to do the same with a 2-object bicategory M, the "walking adjunction". It maps M to a pair of monoidal categories, one of them cartesian C and the other monoidal L. The pseudofunctor produces a monoidal adjunction between them. Its comonad is the ! operator or Ur.

Linear and mixed optics would be the compound optics: the action of the bicategory M in Cat. This is the action that can go between L and C, so it should solve your problem.

I wrote a paper about compound optics and so did Pietro Vertechi. He also introduced Tambara representations for compound optics.

A good source for categorical model of linear types is Benton.

aspiwack commented 5 months ago

For the record, @BartoszMilewski pointed out to me that another approach is to generalise actions from “monoidal categories” to “bicategories”. And shared with me two papers on the subject:

In the latter article, we see the profunctors are generalised to families of profunctors indexed by the category they apply to (so we'd have type EvolvedProfunctor :: Multiplicity -> Type -> Type -> Type). Which, I believe, means that optics would be indexed by two types: category where the structure lives, and category where the focus lives.

I don't actually know that it's a fundamentally different story. The bicategory approach is more general, but this generality may not be useful to us, and probably adds complexity. But I really need to sort this out in my head.

Not today though: I obsessed over this (and other things) yesterday night, and lost sleep over it. I need a step back. I'll be back in a few days when I've calmed down. But leaving this here for future reference.

aspiwack commented 5 months ago

I… I didn't notice that Bartosz posted his message before posting mine :smile: . I had this tab open on my computer and it probably didn't update, then I saw the email notification. I'm excessively amused right now. But anyway, Bartosz articulates the point in much more details than I did. Thank you!

tweag / linear-base