'An arbitrary element' means 'undefined will suffice' point x = fmap (const x) undefined 2009/3/13 Ross Paterson :

On Fri, Mar 13, 2009 at 03:18:15PM +0100, Martijn van Steenbergen wrote:

...

Are there any functors f for which no point/pure/return :: a -> f a exists?

No.  Choose an arbitrary element shape :: f () and define

       point x = fmap (const x) shape _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru

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

On Fri, Mar 13, 2009 at 04:11:57PM +0100, Martijn van Steenbergen wrote:

Eugene Kirpichov wrote:

...

'An arbitrary element' means 'undefined will suffice'

point x = fmap (const x) undefined

Prelude> fmap (const True) undefined :: [Bool] *** Exception: Prelude.undefined

Or is that not what you mean?

OK, an arbitrary maximal element.

Well, yes; then, that means that "an arbitrary element" is also false: you can't just take an arbitrary element and hope that works well. Then the original question must be reformulated: - Are there any functors for which there exists at least one non-bottom value of type 'f a' for some a, but there does not exist a function point :: a -> f a such that (a != _|_) => (point a != _|_). 2009/3/13 Brent Yorgey :

On Fri, Mar 13, 2009 at 05:35:31PM +0300, Eugene Kirpichov wrote:

...

'An arbitrary element' means 'undefined will suffice'

point x = fmap (const x) undefined

This is false.

 Prelude> fmap (const 1) [()]  [1]  Prelude> fmap (const 1) undefined  *** Exception: Prelude.undefined

-Brent

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru

On Sat, 2009-03-14 at 02:12 +1000, Matthew Brecknell wrote:

Ross Paterson wrote:

...

No. Choose an arbitrary element shape :: f () and define point x = fmap (const x) shape

Interesting. Is the arbitrariness of the shape some sort of evidence that Pointed is not really a very useful class in its own right?

A simpler bit of evidence is that the only law I can think of for point (in its own right) is fmap f . point = point . f which we get free anyway. jcc

On 13 Mar 2009, at 14:32, Ross Paterson wrote:

On Fri, Mar 13, 2009 at 03:18:15PM +0100, Martijn van Steenbergen wrote:

...

Are there any functors f for which no point/pure/return :: a -> f a exists?

No. Choose an arbitrary element shape :: f () and define

point x = fmap (const x) shape

Correspondingly, consider the functor Const Void. Cheers Conor