[Haskell-cafe] Existential question

[Tom Schouten]

On 08/18/2011 07:27 AM, oleg at okmij.org wrote:
>> -- Is there a way to make this one work also?
>> data Kl i o = forall s. Kl (i ->  s ->  (s, o))
>> iso :: (i ->  Kl () o) ->  Kl i o
>> iso f = Kl $ \i s ->  (\(Kl kl) ->  kl () s) (f i)
> Yes, if you move the quantifier:
>
> type Kl i o = i ->  Kl1 o
> data Kl1 o = forall s. Kl1 (s ->  (s,o))
> iso :: (i ->  Kl () o) ->  Kl i o
> iso f = \i ->  f i ()
>
> iso1 :: Kl i o ->  (i ->  Kl () o)
> iso1 f = \i ->  (\() ->  f i)
>
Thanks, Oleg.

> I'm not sure if it helps in the long run: the original Kl and mine Kl1
> are useless. Suppose we have the value kl1 :: Kl Int Bool
> with the original declaration of Kl:
>
> data Kl i o = forall s. Kl (i ->  s ->  (s, o))
>
I had simplified the type to make the plumbing simpler.  My intention 
was to include an initial value to use the function as a sequence 
transformer / generator:

data Kl i o = forall s. Kl s (i ->  s ->  (s, o))


This is an Arrow.  At first I wondered if there was also an associated 
Monad, hence the iso function.  From your reply and Ryan's comment it 
seems that making a Monad instance for

data Kl1 o = forall s. Kl (s -> (s,o))

is not possible because its bind function cannot be typed as the (i -> 
Kl1 o) function introduces a value -> type dependency.


Does the "growing type" s1 -> s2 -> (s1,s2) in the bind-like method 
below support some other abstraction that is monad-like?

data Kl1' s o = Kl1' (s -> (s,o))

bind' :: (Kl1' s1 i) -> (i -> Kl1' s2 o) -> (Kl1' (s1,s2) o)

bind' mi f = Kl1' mo where
   mo (s1,s2) = ((s1',s2'),o) where
     (Kl1' u1) = mi
     (s1', i)  = u1 s1
     (Kl1' u2) = f i
     (s2', o)  = u2 s2