Why do we need Control.Lens.Reified?

Question

Why do we need Control.Lens.Reified? Is there some reason I can't place a Lens directly into a container? What does reify mean anyway?

Answer 1

We need reified lenses because Haskell's type system is predicative. I don't know the technical details of exactly what that means, but it prohibits types like

[Lens s t a b]

For some purposes, it's acceptable to use

Functor f => [(a -> f b) -> s -> f t]

instead, but when you reach into that, you don't get a Lens; you get a LensLike specialized to some functor or another. The ReifiedBlah newtypes let you hang on to the full polymorphism.

Operationally, [ReifiedLens s t a b] is a list of functions each of which takes a Functor f dictionary, while forall f . Functor f => [LensLike f s t a b] is a function that takes a Functor f dictionary and returns a list.

As for what "reify" means, well, the dictionary will say something, and that seems to translate into a rather stunning variety of specific meanings in Haskell. So no comment on that.

Answer 2

The problem is that, in Haskell, type abstraction and application are completely implicit; the compiler is supposed to insert them where needed. Various attempts at designing 'impredicative' extensions, where the compiler would make clever guesses where to put them, have failed; so the safest thing ends up being relying on the Haskell 98 rules:

• Type abstractions occur only at the top level of a function definition.
• Type applications occur immediately whenever a variable with a polymorphic type is used in an expression.

So if I define a simple lens:[1]

lensHead f [] = pure []
lensHead f (x:xn) = (:xn) <$> f x

and use it in an expression:

[lensHead]

lensHead gets automatically applied to some set of type parameters; at which point it's no longer a lens, because it's not polymorphic in the functor anymore. The take-away is: an expression always has some monomorphic type; so it's not a lens. (You'll note that the lens functions take arguments of type Getter and Setter, which are monomorphic types, for similar reasons to this. But a [Getter s a] isn't a list of lenses, because they've been specialized to only getters.)

What does reify mean? The dictionary definition is 'make real'. 'Reifying' is used in philosophy to refer to the act of regarding or treating something as real (rather than ideal or abstract). In programming, it tends to refer to taking something that normally can't be treated as a data structure and representing it as one. For example, in really old Lisps, there didn't use to be first-class functions; instead, you had to use S-Expressions to pass 'functions' around, and eval them when you needed to call the function. The S-Expressions represented the functions in a way you could manipulate in the program, which is referred to as reification.

In Haskell, we don't typically need such elaborate reification strategies as Lisp S-Expressions, partly because the language is designed to avoid needing them; but since

newtype ReifiedLens s t a b = ReifiedLens (Lens s t a b)

has the same effect of taking a polymorphic value and turning it into a true first-class value, it's referred to as reification.

Why does this work, if expressions always have monomorphic types? Well, because the Rank2Types extension adds a third rule:

• Type abstractions occur at the top-level of the arguments to certain functions, with so-called rank 2 types.

ReifiedLens is such a rank-2 function; so when you say

ReifiedLens l

you get a type lambda around the argument to ReifiedLens, and then l is applied immediately to the the lambda-bound type argument. So l is effectively just eta-expanded. (Compilers are free to eta-reduce this and just use l directly).

Then, when you say

f (ReifiedLens l) = ...

on the right-hand side, l is a variable with polymorphic type, so every use of l is immediately implicitly assigned to whatever type arguments are needed for the expression to type-check. So everything works the way you expect.

The other way to think about is that, if you say

newtype ReifiedLens s t a b = ReifiedLens { unReify :: Lens s t a b }

the two functions ReifiedLens and unReify act like explicit type abstraction and application operators; this allows the compiler to identify where you want the abstractions and applications to take place well enough that the issues with impredicative type systems don't come up.

[1] In lens terminology, this is apparently called something other than a 'lens'; my entire knowledge of lenses comes from SPJ's presentation on them so I have no way to verify that. The point remains, since the polymorphism is still necessary to make it work as both a getter and a setter.