Is the functor distribution law for the `Alt` typeclass trivial?

user_1726343 0
Viewed 212

I was looking at the laws for the Alt typeclass, which looks like this:

class Functor f => Alt f
  where
  (<!>) :: f a -> f a -> f a

One of the laws goes like this:

<$> left-distributes over <!>:  f <$> (a <!> b) = (f <$> a) <!> (f <$> b)

More verbosely, this is:

fmap f $ (<!>) a b = (<!>) (fmap f a) (fmap f b)

Let's say we uncurry the <!> operation, i.e. that we suppose the class is written like this:

class Functor f => Alt f
  where
  alt :: (f a, f a) -> f a

We can write a combinator like this:

mapBoth :: Functor f => (a -> b) -> (f a, f a) -> (f b, f b)
mapBoth f = bimap (fmap f) (fmap f)

This represents the composition of the type Pair a = (a, a) functor with a given functor f. So it is itself the morphism mapping of a functor.

The law in question can now be written (without changing its meaning) like this:

fmap f . alt = alt . mapBoth f

Note that the mapBoth f is simply applying fmap f to both of the arguments of alt, as in the original statement of the law.

This is akin to demanding that alt is a natural transformation from the functor (f -, f -) to the functor f -.

However, isn't it actually impossible for a function of alt's type not to be a natural transformation? How would one write a "bad" implementation of alt that that typechecks, but would be rejected by the law?

free-theorem functor haskell
2 Answers

While it isn't the consensus of the other answers and comments, this is not a natural property of "real-world" Haskell.

It is helpful to developers who write non-parametric code to know when they should add constraints to remain compatible with code which takes parametricity for granted.

A badly-behaved example

{-# LANGUAGE GADTs #-}

data Badly a where
  End :: a -> Badly a
  Cons :: a -> Badly b -> Badly a

(<++>) :: Badly a -> Badly b -> Badly a
(End a)    <++> r = Cons a r
(Cons a l) <++> r = Cons a (l <++> r)

instance Functor Badly where
  fmap f (End a) = End (f a)
  fmap f (Cons a r) = Cons (f a) r

instance Alt f where
  (<!>) = (<++>)
user_59472470

Yes the law holds for free, by parametricity.

Even then, these laws still have value.

  1. It allows people to be aware of them without being adepts of programming language theory.

  2. You will want to have these laws around if you port these interfaces to languages with weaker type systems.

  3. Until Haskell is actually given formal semantics, we technically don't know that those free theorems hold. By sufficiently high standards of formality, it's not enough to pretend that Haskell is a pure polymorphic lambda-calculus. So we might as well add and check these "free" laws just in case.

user_68637490
Related