On 08/18/2011 07:27 AM, oleg@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