Lenses in Idris

I’ve been pretty comfortable with using Haskell’s lenses for a while now, but until recently I hadn’t understood what they are or how to make them. A couple weeks ago I was reading Yet Another Lens Blog Post (I don’t remember which), and it just… clicked. I don’t mean this to be one of those, but I’ll just mention the metaphor that clicked for me because I think it’s cool: a lens is a machine that accepts a smaller machine and attaches to the structure, then uses some complicated system of chains and pulleys to move the smaller machine around and apply it at some point in the structure. You can use a lens as a “setter” by inserting a machine that performs some modification to the structure; you use it as a “getter” by inserting a camera. And of course, you can also insert another lens into the machine, which will attach to the point-in-the-structure that the larger lens brings it to and accept another machine.

But again, that metaphor was more for entertainment purposes than didactic. I don’t expect it to make lenses click for anyone. What I want to do in this blog post is to use my newfound understanding to implement lenses in Idris!

Let’s start by defining the type synonym. Except Idris doesn’t have type synonyms; they’re subsumed by type functions.

Lens : Type -> Type -> Type -> Type -> Type
Lens s t a b = (f : Type -> Type) -> Functor f -> (a -> f b) -> s -> f t

This differs in two respects from the standard Haskell type synonym. First, we don’t need any extensions because Idris naturally supports explicit abstraction over types!

…but also, since Idris doesn’t have any notion of polymorphism except for explicit abstraction over types, the functor and its typeclass instance must be arguments to our function. Normally this is handled using implicit arguments, which look like Haskell’s external notion of polymorphism, but they’re not applicable here because only top-level names can have implicit arguments. I usually prefer Idris-style polymorphism over Haskell-style polymorphism, but in this case it’s a little awkward.1

Anyway, let’s move on. Can we write a lens now?

first : Lens (a, c) (b, c) a b
first F inst f (a, b) = map (x => (x, b)) (f a)

Some notes:
* We’re introducing the functor and instance as F and inst. We don’t actually have to use them anywhere: since inst is the only typeclass instance in scope with the appropriate type, Idris automatically knows to use its methods.
* We’re calling it first instead of the more traditional _1 because Idris doesn’t seem to allow names to start with _.
* There’s no fmap! In Idris, map is a functor method. Also, we use => for lambdas instead of ->.

Now that we have a lens, we can use it just like we’d use one in Haskell:

-- %instance invokes standard instance search
> first Maybe %instance Just (5, "hello")
Just (5, "hello") : Maybe (Integer, String)

But it’s not quite as nice as raw Haskell lenses are, because of those two extra arguments. So let’s write the functions to use a lens as a getter, modifier, or setter:

-- this instance isn't in the standard library for some reason
instance Functor (const a) where map f = id

-- This is cool: we don't need a special `Const` type, we can just use the Functor instance
-- for the standard `const : a -> b -> a` (in this case, `const : Type -> Type -> Type`).
-- Dependent types can be fun! (Also, no wrapping/unwrapping.)
view : Lens s t a b -> s -> a
view {a} l = l (const a) %instance id

-- Same thing here: we use the regular identity function instead of defining an Identity newtype, and that means no need to wrap and unwrap!
over : Lens s t a b -> (a -> b) -> s -> t
over l f = l id %instance f

set : Lens s t a b -> b -> s -> t
set l val = over l (const val)

Here's one more wrinkle. In Haskell, lenses have the cool property that they can be composed using the standard function composition operator, and it works exactly how you'd expect a dedicated lens composition operator to work. Can we do this in Idris?

> over (first . first) (++"!") (("hello", "there"), "world")
-- I guess we can't.

Remember when we defined our "type synonym" and we had to have those two extra arguments at the beginning? That's what's getting in the way here. We'll need to abstract over the functor and instance before composing them; Haskell's polymorphism machinery handles that transparently.

-- I don't actually know what fixity it should have
infixl 5 ..
(..) : Lens s t a b -> Lens a b a' b' -> Lens s t a' b'
l .. m = \f : Type -> Type, inst : Functor f => l f inst . m f inst

> over (first .. first) (++"!") (("hello", "there"), "world")
Error: no such variable b.

…huh. That doesn’t sound like an error we should be getting from any language that does scoping analysis! It seems like we may have run into… a bug in Idris!

Perhaps soon I can resolve this or bring it to someone’s attention to get it resolved. For now, it looks like this post will have to end with a cautionary tale about young programming languages instead of a working Lens library. Oh well!

  1. I think it might be possible to allow expressions to have implicit arguments by lifting any unfilled arguments from an “incomplete term” out to the top level and quantifying over them explicitly there, but it seems like it would be a difficult transformation to do well… and I’m not sure it would even give the desired behavior here anyway. 

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s