Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why does “failing” (from lens) produce invalid traversals?

From the documentation:

Try the first Traversal (or Fold), falling back on the second Traversal (or Fold) if it returns no entries.

This is only a valid Traversal if the second Traversal is disjoint from the result of the first or returns exactly the same results.

Is there a simple example of an invalid traversal generated by failing and a test case demonstrating it?

like image 551
Artyom Avatar asked Nov 25 '14 23:11

Artyom


1 Answers

For the counterexample, let us first define a new data type, for which we generate traversals using makePrisms:

data T = A T | C deriving Show
makePrisms ''T

_A :: Traversal T T is now a valid traversal. Now, construct a new traversal using failing:

t :: Traversal' T T
t = failing _A id

Notice that (C & t .~ A C) ^.. t = [C], which looks like it fails a traversal law (you don't "get what you put in"). Indeed, the second traversal law is:

fmap (t f) . t g ≡ getCompose . t (Compose . fmap f . g)

which is not satisfied, as can be seen with the following choice for f and g:

-- getConst . t f = toListOf t
f :: T -> Const [T] T
f = Const . (:[])

-- runIdentity . t g = t .~ A C
g :: T -> Identity T
g = pure . const (A C)

Then:

> getConst . runIdentity . fmap (t f) . t g $ C
[C]

While:

> getConst . runIdentity . getCompose . t (Compose . fmap f . g) $ C
[A C]

So there is indeed a case where failing with valid traversals doesn't produce a valid traversal.

like image 50
bennofs Avatar answered Oct 10 '22 11:10

bennofs