The big picture

Strategic programming

Generalized “visiting”

Structure shy programming

Programming in a pattern-match style. You have a tree of data, and you pattern-match against it.

To borrow an example from the paper, a program that lists all movies in an XML file by recursively searching for all <Movie> tags and looking at their <title> child, is a structure shy program.

If you have a particular schema in mind, however, you can optimize a structure shy program by using information from the schema. If you know there’s no need to search inside the <Reviews> tag to find <Movie>s, and you know that <Movie> tags cannot appear inside themselves, you can save a lot of time and potentially avoid a full recursive search.

Why bother programming in the structure-shy way, when optimizing these programs is so easy?

In a functional programming setting, we might classify structure-shy programs into two categories:

These correspond to structure-preserving “maps” and structure-flattening “folds”; I think the distinction is important in FP.

Optics

Concrete form

In the concrete representation, a lens is a pair of two functions, for example

structure Lens' (whole part : Type) where
  view: whole → part
  update: whole → part → whole

Then we can lift a function from parts → parts into a function from wholes → wholes, like this:

def lens'Map {whole part : Type} (lens: Lens' whole part) (w : whole) (f : part → part) : whole :=
  (lens.view w) |> f |> (lens.update w ·)
-- assume fstLens' is a Lens' onto the first element of a pair

def coolPair := ("banana", 5)
##eval lens'Map fstLens' coolPair String.toUpper -- ("BANANA", 5)

Benefits

Easy to explain, easy to write.

Drawbacks

These are function pairs, not functions. Composing lenses is hard; you need a special function that takes two lenses and returns a third lens representing their composition.

They don’t play nice with other optics like prisms.

var Laarhoven but ignoring the functors

abbrev CrapLens (whole part: Type) := (part → part) → (whole → whole)

If I’m a CrapLens whole part, I can take any function from parts to parts and turn it into a function from wholes to wholes. Naturally, you do this the same way lens'Map was written:

You zoom into a structure, apply the function, then zoom out. A lens.

How else would you write a function with this signature? (Especially if these were type-changing lenses?)

van Laarhoven

Stick a functor in there. Any old functor. (In Haskell I believe you’d represent this with a forall?)

abbrev Lens (whole part: Type) [Functor f] := (part → f part) → (whole → f whole)

Alright, so this says if I’m a Lens, I can take any function from “a part” to “a part in any computational context”, and turn it into a function from “a whole” to “a whole in the same computational context”.

Given that we don’t have anything like Applicative or Monad’s pure, the only way to “get into the computational context” is to apply the function; then to reassemble into the whole, the only thing we can do is fmap. A bit like solving a crossword puzzle.

Why stick a functor in there? - Should look into this. I think the answer is: with CrapLens we can only write a lens, but the functor in Lens provides just enough flexibility to generalize to a few other types of optic.

Type-changing lenses

Who says a lens has to update things to the same type? For example you could update a Prod String Nat into a Prod Nat Nat by taking the length of the first element. Why not.

You end up with a lot of type variables floating around but it’s not so bad.

abbrev CrapLens (whole whole' part part': Type)             := (part →   part') → (whole →   whole')
abbrev Lens     (whole whole' part part': Type) [Functor f] := (part → f part') → (whole → f whole')

Lenses that take wholes to whole's by way of taking parts to part's.

Profunctors, in general

Roughly speaking, something that “consumes As and produces Bs”. Importantly this “produces” means something more general than “has the type B exactly”.

A function A → B is a profunctor, but so is A → (B, C), and A → (B, B), as well as A → List B and A → Maybe B, and even A → F B for any functor F

The actual typeclass is something like

class Profunctor (p : Type u → Type v → Type w) where
  dimap : {α α' : Type u} → {β β' : Type v} → (α' → α) → (β → β') → (p α β) → (p α' β')

Note that the first argument is (α' → α) and the second argument is (β → β'). This is consistent with the idea that a p α β is something that “takes αs to βs” - the arguments to dimap are the correct way around to be thought of as “pre-” and “post-processors”. To turn a p α β into a p α' β':

Now the laws make sense:

Summary

Profunctor α β is a generalization of “function from α to β” where α or β might have additional “context” (say, α → (β, χ)) or be in any functor (say, a → List β).

Cartesian profunctors

….