(WIP) A mess of new concepts

[b-mehta]

WIP:

• needs a lot of tidying up
• needs rebasing after merge of #44
• needs documentation to explain some of the below

Changes introduced:

• There are two sorts of traversable: Prelude.Traversable t in which

traverse :: Prelude.Applicative e => (a -> e b) -> t a -> e (t b)

or Data.Traversable t in which

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

So, there should be two notions of a Traversal, and there must be two versions of the Wandering type class. Here, due to lack of imagination, they are prefixed P and D.

• • More linearity for get and set. Naturally, these two cannot be linear as usually written: get discards part of its argument, and set throws away the old information. However they can be given type signatures which reflect these facts and are stronger than just non-linear arrows. Setting is easy to deal with: we can just return the original value that was replaced, then running snd afterwards recovers the non-linear set. The idea is that set' can have a type signature that promises more, but degrades nicely to the standard one.

  • Getting is a little more complex: We define a 'wastebasket' of resources, Top, which has the property that forall x. x ->. Top is inhabited (uniquely). It thus forms a (linear) monoid. The use of Top here is that arrows a ->. (Top, b) are something of an intermediate between a ->. b and a -> b; they promise that a is not used more than once, but can't promise that all of a is used. For example, we can define (a,b) ->. (Top, b), which gets the second component and 'throws away' the first component. Again, if the extra linearity promise isn't helpful, post-composing with snd will recover the usual get. (Aside: the writer monad writing to Top has its Kleisli arrows as the above arrows, so we can nicely compose these functions: maybe there is some use to a promise that the argument is used no more than once)

To write: the lens constructor and a deconstructor? Pair. Wrapped semigroups

[b-mehta]

Idea: Lenses have type forall f. Control.Functor f => (s, f b)->. (a, f t) Const Top is a control functor which will extract the get part, and identity recovers set. The fact that all control functors are strong means any valid lens can be written like this

[b-mehta]

Nope: the correct linear rank-1 form of a lens is s ->. (a, b ->. t)

[b-mehta]

note to self: try having both pwander and dwander in Wandering, and see what breaks: they might not really need to be distinct

[b-mehta]

@Divesh-Otwani Apologies for leaving this (and other branches) in such a state. Feel free to get in touch with me if you'd like some help tidying it up or just a better idea of what was going through my head with some of the stuff I left unfinished!

[Divesh-Otwani]

@b-mehta Thanks -- will get in touch!

[aspiwack]

For most of the things introduced here, see #79 . Which covers the same ground except:

• The traversal story is different there
• There is no getters with Top

I'm not convinced the getters with Top are much useful at all: after all once you have a linear Top value, then you have to carry it around. You can never get rid of it. Until it is promoted to being unrestricted. So, really, the only use of the Top-based getters would be to define the unrestricted getters, except less efficiently.

I'm leaving the PR open, still, as an inspiration as I'm trying to tackle the traversal story. See also #190 (and soon more).