[Haskell-cafe] Pointless functors

[Dan Doel]

On Thursday 12 March 2009 10:30:47 pm Robin Green wrote:
> For most functors, that is equivalent to
>
> point x = undefined
>
> But by that logic, everything is a member of every typeclass...

There are some cases where expected laws will prevent that. For instance, If 
you try to make a monad like:

  instance Monad m where
    return  = undefined
    m >>= f = undefined

Then it will fail the law:

  m >>= return = m

unless the only possible value of m is undefined (that is, m a is uninhabited 
except for bottom).

In the case of pointed functors, the point is supposed to be a natural 
transformation from the identity functor to the functor in question, so:

  fmap f . point = point . f

which always works with 'point = undefined' as long as 'fmap f' is strict 
(which it's basically required to be, since it must satisfy fmap id = id, and 
id is strict).

Of course, the fact that it satisfies the relevant law doesn't make it less 
worthless as an instance. To make things less trivial, one might restrict 
himself to definitions that would work in a total language, and then it's easy 
to come up with examples of functors that aren't pointed. For instance, one 
can write the following in Agda:

  data Void (a : Set) : Set where -- empty

  mapVoid : {a b : Set} -> (a -> b) -> Void a -> Void b
  mapVoid f ()  -- empty function

  pointVoid : {a : Set} -> a -> Void a
  pointVoid = ? -- can't be written

-- Dan