Home > Back-end >  Law of naturality for list Traversable instance
Law of naturality for list Traversable instance

Time:07-21

A Traversable instance must satisfy 3 laws: Naturality, Identity, Composition. The naturality law states that:

t . traverse f = traverse (t . f)

But for the following examples, this does not hold true.

Example 1

t (Just a) = Left a
f = Just 
s = "string"

\> t . traverse f $ s
  Left "string"
\> traverse (t . f) s 
  Left 's'

One might argue that (Either a b) is applicative in b, not in a, but still, this example disproves that the law of naturality is satisfied by the Traversable instance for [].

Example 2

t (head : tail) = replicate 2 head
f = (:[])
s = "string"

\> t . traverse f $ s
  ["string", "string"]
\> traverse (t.f) s 
  ["string", "string", ...., "string"]
-- a list with 64 elements
-- equivalent to: replicate 64 "string"

This is due to the nature (behaviour) of list`s Applicative listance. It forms a cartesian product between the lists.

So, for the ZipList datatype this law holds, because it`s Applicative instance behaves differently ( one could say 'properly' - from the point of view of traverse and sequenceA respecting their Naturality laws).

Could someone clarify to me what am I doing/ seeing wrong, so that I could understand why the Traversable instance for [] is law-abiding?

CodePudding user response:

There is an explicit condition that t must be an applicative transformation. Here's the full documentation:

Laws

A definition of traverse must satisfy the following laws:

Naturality

t . traverse f = traverse (t . f) for every applicative transformation t

[...]

where an applicative transformation is a function

t :: (Applicative f, Applicative g) => f a -> g a

preserving the Applicative operations, i.e.

t (pure x) = pure x
t (f <*> x) = t f <*> t x

[some emphasis added]

The t functions in your examples are not applicative transformations. They don't preserve pure:

t (pure x) = Left x /= Right x = pure x
t (pure x) = [x,x] /= [x] = pure x
  • Related