Application of `view` to a lens does not always type check.

[kindaro]

see for yourself

% cabal repl --verbose=0 --build-depends lens
λ import Control.Lens
λ let example ∷ Lens () () Int Bool
>     example = undefined
>
λ :type view example

<interactive>:1:6: error:
    • Couldn't match type ‘Bool’ with ‘Int’
      Expected: Getting Int () Int
        Actual: (Int → Const Int Bool) → () → Const Int ()
    • In the first argument of ‘view’, namely ‘example’
      In the expression: view example

what should happen

This application should type check, giving the type () → Int. A suitable function is defined like so:

λ stare lens = getConst . lens Const
λ :type stare example
stare example ∷ () → Int

This is the standard definition of view, is it not? I expected it to be offered by lens.

[phadej]

example ∷ Lens () () Int Bool

is invalid type.

The four arguments of an optic are not independent (there was @ekmett's blog post explaining it, but I fail to find it right now).

One way to think it is: with your example, the lens laws fail to type-check (even if you relax the type of view), so it's not unexpected that view does too.

The practical reason for view to have restricted type is to resolve ambiguity. view uses only two arguments of a polymorphic lens, so if the other two are not pinned somehow, the program won't type-check either.

[kindaro]

I guess you mean this blog post: http://comonad.com/reader/2012/mirrored-lenses/. Right?

However, I do want to have a lens that is not «well behaved», and I do want to view it. How about we add a function such as stare to lens? It works fine for my use cases so far.

[ekmett]

The problem is this. I can't generalize the common combinator.

view used to have a more general type. After all it doesn't need to care what type you would 'put back. But letting the other argument float to any type means that you wind up with a ton of lenses that need explicit type arguments in order to function. Consider one that converts to/from JSON. Now when you go to view it you need to tell it what type you aren't using it to construct at the same time you view. This rendered the library more or less unusable.

As a result, and because these combinators aren't required for any lawful use of lenses, I removed the concept of a "Getting" that didn't have source and target match. Otherwise I'd have to name nearly twice as many things, half of which would confuse the typical user by their presence, and which don't work well or at all with the rest of the lenses I do provide.

Just like with lens-based-zippers and effects they eventually got exiled to "someone else's problem" given there was no requirement for them to be implemented in the package on one hand, and them being actively harmful to comprehension on the other. Unlike the zippers and effects, there's currently no package supplying them.

You can of course implement this by going through the lens with getConst . l Const or any of a half-dozen other ways using other combinators in the library for working with holes and reflection and the like, but I view supplying it as an active disservice to the bread-and-butter consumers of the library.

[ekmett]

Closing