On 9/13/10 6:23 PM, Paolo G. Giarrusso wrote:

Then, I would also like to understand what exactly a strict functor is, in detail, and/or a link to the post you reference.

I'm assuming the OP was referring to a functor for strictness I mentioned recently in the discussion about pointed functors. That is, newtype Strict a = Strict a instance Functor Strict where -- This isn't a lawful endofunctor fmap f (Strict a) = Strict (f $! a) instance Pointed Strict where -- This isn't lawful either, as an endofunctor point = Strict The idea being that we make all applications strict. However, that definition of fmap isn't lawful because we don't have that fmap(f . g) = (fmap f).(fmap g) for all f and g. In particular, it fails when (f . g) is bottom eating, i.e. when (g x == _|_) =/=> (f (g x) == _|_). We can, however, define strict composition: (f .! g) x = f $! g x And we do have that fmap(f .! g) = (fmap f).(fmap g) for Strict. So, Strict is a (category theoretic) functor, it's just not an endofunctor on Hask. Given that any functor for adding strictness will have to deal with the same issue of preserving bottom-eating compositions, I postulated that there exists no functor from (all of) Hask to !Hask. But, since !Hask is a subcategory of Hask, it's trivial to go the other direction. In fact, the Strict defined above can be considered as the inclusion functor from !Hask to Hask by making the strictness of !Hask explicit. This also allows Strict to be considered a pointed functor since fmap f . point = point . f for strict functions f. I haven't looked through the suggested code to see if it can actually work around the problem. -- Live well, ~wren

Sjoerd Visscher wrote:

But StrictIncl can't be a pointed functor, only endofunctors can be pointed.

Could someone tell me what exactly a pointed functor is? I googled but did not find a definition. Thanks Ben

Román González wrote:

On Thu, Sep 16, 2010 at 2:12 PM, Ben Franksen wrote:

...

Sjoerd Visscher wrote:

...

But StrictIncl can't be a pointed functor, only endofunctors can be pointed.

Could someone tell me what exactly a pointed functor is? I googled but did not find a definition.

Here you will find what a Pointed Functor would be => http://haskell.org/sitewiki/images/8/85/TMR-Issue13.pdf

Look up for the Typeclassopedia, start reading functor, next thing you will find is the Pointed typeclass

Thanks for the link. What I actually wanted was a mathematical definition, though. From the TMR article I gather that a pointed functor could be defined as an endo-functor F: C -> C together with a natural transformation pure: Id -> F where Id: C -> C is the identity functor. No additional laws (beside naturality of pure) are imposed. Right so far? Why is this an interesting structure? Cheers Ben

On Sep 17, 2010, at 10:39 PM, Ben Franksen wrote:

What I actually wanted was a mathematical definition, though.

Here's a definition of pointed objects: http://ncatlab.org/nlab/show/pointed+object -- Sjoerd Visscher sjoerd@w3future.com

On Saturday 18 September 2010 6:03:39 pm wren ng thornton wrote:

pointed objects, pointed sets/groups/topospaces, pointed categories, pointed functors, etc aren't all the same though.

The definition of pointed objects could be massaged to yield pointed functors, though. Instead of a category with a terminal object, we could relax the definition to include categories with a distinguished object I. Then, a pointed object in such a category is an object X together with x : I -> X. This isn't always very interesting. For any category with an initial object 0, the category of objects pointed over 0 is isomorphic to the original category, for instance. However, categories with arbitrary distinguished objects could be viewed as a precursor to monoidal categories, and pointed objects are then precursors to monoid objects. And then when you instantiate all that to the category of endofunctors over some category, you get pointed functors being precursors to monads. -- Dan

On Tue, 2010-09-14 at 11:27 +0100, Neil Brown wrote:

On 13/09/10 17:25, Maciej Piechotka wrote:

...

...

import Control.Exception import Foreign import Prelude hiding (catch)

data StrictMonad a = StrictMonad a deriving Show

instance Monad StrictMonad where return x = unsafePerformIO $ do (return $! x) `catch` \(SomeException _) -> return x return $! StrictMonad x StrictMonad v>>= f = f v

It seems to be valid IMHO Functor and Monad (I haven't prove it) as long as functions terminates.

I'm not sure if I'm allowed to use unsafePerformIO in my counter-example, but you used it so why not ;-) The first monad law says: "return a >>= k = k a"

let k = const (StrictMonad ()) a = unsafePerformIO launchMissiles

In "k a" no missiles will be launched, in "return a >>= k", they will be launched.

I guess we enter a grey area - I did use unsafePerformIO but without side-effects.

You can construct a similar example against "m >>= return = m".

Assuming StrictMonad (constructor) is hidden - I don't think so.

Although, if you changed your definition of bind to:

StrictMonad v >>= f = return v >>= f >>= return

Then as long as "return x >>= return = return x" (which it does for you) then you automatically satisfy the first two monad laws! Which is an interesting way of solving the problem -- haven't checked the third law though.

My error.

Thanks,

Neil.

Regards