
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))
That change makes a world of difference! For example, the above type (Kl i) is clearly a monad
instance Monad (Kl i) where return x = Kl () (\_ s -> (s,x)) (Kl s m) >>= f = Kl s (\i s -> case f (snd (m i s)) of Kl s' m' -> (s,snd (m' i s')))
It is the Reader monad. Different Kl values have their own, private s. The quantification ensures that each encapsulated 's' applies only to its generator. Therefore, we can just as well apply that 's' right at the very beginning. Therefore,
data Kl i o = forall s. Kl s (i -> s -> (s, o))
is essentially
data Kl' i o = Kl' (i -> o)
which is certainly and Arrow and a Monad. We do not need existential at all. The web page http://okmij.org/ftp/Computation/Existentials.html describes other eliminations of Existentials.
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
Not all things are monads; for example, restricted and parameterized monads are not monads (but do look like them, enough for the do-notation). Your Kl1' does look like another generalization of monads. I must say that it seems to me more fitting for a parametrized applicative:
class Appish i where purish :: a -> i s a appish :: i s1 (a ->b) -> i s2 a -> i (s1,s2) b
data KL s a = KL (s -> (s,a))
instance Appish KL where purish x = KL (\s -> (s,x)) appish (KL f1) (KL f2) = KL $ \(s1,s2) -> let (s1', ab) = f1 s1 (s2', a) = f2 s2 in ((s1',s2'), ab a)