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