[Haskell-cafe] Pointless functors
Dan Doel
dan.doel at gmail.com
Fri Mar 13 11:50:14 EDT 2009
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
More information about the Haskell-Cafe
mailing list