CODEWITHSUNDEEP
haskellhaskell-lens
George
George

Reputation: 7317

Justifying a Type Equivalency Asserted in Haskell Lens Library

According to the tutorial on Lenses:

type Getting b a b  = (b -> Const b b) -> (a -> Const b a)

-- ... equivalent to: (b ->       b  ) -> (a ->       b  )

-- ... equivalent to:                     (a ->       b  )

Question: Why is (b -> b) -> (a -> b) equivalent to (a -> b)?

Upvotes: 2

Views: 88

Answers (2)

dfeuer
dfeuer

Reputation: 48591

The tutorial isn't very precise about this. Here's the full definition of Getting:

type Getting r s a = (a -> Const r a) -> s -> Const r s

Stripping off the newtype noise,

Getting r s a ~= (a -> r) -> s -> r

The interesting isomorphism you should get from this is the following:

(forall r. Getting r s a) ~= s -> a

In a now-deleted comment, chi pointed out that this is a special case of the Yoneda lemma.

The isomorphism is witnessed by

fromGetting :: Getting a s a -> (s -> a)
fromGetting g = getConst . g Const
           -- ~= g id

-- Note that the type of fromGetting is a harmless generalization of
-- fromGetting :: (forall r. Getting r s a) -> (s -> a)

toGetting :: (s -> a) -> Getting r s a
toGetting f g = Const . getConst . g . f
           -- ~= g . f

-- Note that you can read the signature of toGetting as
-- toGetting :: (s -> a) -> (forall r. Getting r s a)

Neither fromGetting nor toGetting has a rank-2 type, but to describe the isomorphism, the forall is essential. Why is this an isomorphism?.

One side is easy: ignoring the Const noise,

  fromGetting (toGetting f)
= toGetting f id
= id . f
= f

The other side is trickier.

  toGetting (fromGetting f)
= toGetting (f id)
= \g -> toGetting (f id) g
= \g -> g . f id

Why is this equivalent to f? The forall is the key here:

f :: forall r. Getting r s a
  -- forall r. (a -> r) -> s -> r

f has no way to produce an r except by applying the passed function (let's call it p) to a value of type a. It's given nothing but p and a value of type s. So f really can't do anything except extract an a from the s and apply p to the result. That is, f p must "factor" into the composition of two functions:

f p = p . h

So

g . f id = g . (id . h) = g . h = f g

Upvotes: 10

Benjamin Hodgson
Benjamin Hodgson

Reputation: 44634

The type says "You give me a b -> b and an a, and I'll give you a b." What can a function with that type do with its b -> b? Two options:

  1. Ignore the function altogether
  2. Apply it to a b

How do you get hold of a b to apply the function to? You use the a to produce one. So either way, it has to do the work of an a -> b.

Here's some code to witness the (edit: not-quite) isomorphism.

in :: ((b -> b) -> a -> b) -> (a -> b)
in f x = f id x

out :: (a -> b) -> ((b -> b) -> a -> b)
out f g x = g (f x)

Upvotes: 1

Related Questions