[Haskell-cafe] Applicative but not Monad

[Dan Weston]

Obviously you know what your talking about and I don't, so this is a 
question purely out of ignorance.

It seems to me that Tomorrow cannot be parametrically polymorphic, or 
else I could wrap it again (Tomorrow (Tomorrox x)). An unwrapping 
fixpoint operator needs to reflect the type to know when not to go too 
far. One solution is to guarantee that it can go as far as it wants with 
a comonad (stopping when the function argument wants to, not when the 
data type runs out of data):

import Control.Comonad
import Control.Monad.Fix

tfix :: Comonad tomorrow => (tomorrow x -> x) -> x
tfix = extract . (\f -> fix (extend f))

To quote Cabaret, if tomorrow belongs to me, then surely the day after 
belongs to me as well.

Otherwise, to stop the fixpoint, it seems you need a more restricted 
type to encode some stopping sentinel (my own parametrically polymorphic 
attempts all end in infinite types, so maybe ad hoc polymorphism or a 
type witness is needed?)

Do you have a blog post on this problem?

Dan

Conor McBride wrote:
> On 2 Nov 2009, at 00:11, Ross Paterson wrote:
> 
>> On Sun, Nov 01, 2009 at 04:20:18PM +0000, Conor McBride wrote:
>>> On 31 Oct 2009, at 10:39, Conor McBride wrote:
>>>> I have an example, perhaps not a datatype:
>>>> tomorrow-you-will-know
>>> Elaborating, one day later,
>>>
>>>  if you know something today, you can arrange to know it tomorrow
>>>  if will know a function tomorrow and its argument tomorrow, you
>>>    can apply them tomorrow
>>>  but if you will know tomorrow that you will know something the
>>>    day after, that does not tell you how to know the thing tomorrow
>> Yes, but if you will know tomorrow that you will know something
>> tomorrow, then you will know that thing tomorrow.
> 
> That depends on what "tomorrow" means tomorrow.
> 
>> The applicative does coincide with a monad, just not the one you first
>> thought of (or/max rather than plus).
> 
> True, but it's not the notion I need to analyse circular programs.
> I'm looking for something with a fixpoint operator
> 
>    fix :: (Tomorrow x -> x) -> x
> 
> which I can hopefully use to define things like
> 
>    repmin :: Tree Int -> (Int, Tomorrow (Tree Int))
> 
> so that the fixpoint operator gives me a Tomorrow Int which I
> can use to build the second component, but ensures that the
> black-hole-tastic Tomorrow (Tomorrow (Tree Int)) I also receive
> is too late to be a serious temptation.
> 
> All the best
> 
> Conor
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
>