Tom Schouten tom at zwizwa.be
Sat Aug 20 23:26:44 CEST 2011

```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
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

```