[<<][meta][>>][..]Sat Aug 20 20:11:59 CEST 2011

( Not sent. Trying to answer it myself first. ) 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) > > > 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)) > > Now, what we can do with kl1? We can feed it an integer, say 1, and > obtain function f of the type s -> (s,Bool) for an _unknown_ type s. > Informally, that type is different from any concrete type. We can > never find the Bool result produced by that function since we can > never have any concrete value s. The only applications of f that will > type check are > \s -> f s > f undefined > both of which are useless to obtain f's result. Thanks, Oleg. The real data type I intend to use is this one: data Kl1 o = forall s. Kl1 s (s -> (s,o)) Kl1 then represents infinite sequences of values of type o, and functions of type i -> s -> (s, o) can then represent sequence operators. (Monad and Kleisli arrow). The reason I left it out is that it makes the plumbing more awkward. The original problem I'm trying to solve is that I can't seem to write down composition of the Kleisli arrows, or the bind or join operation in the monad, without running into typing problems. Everything works fine for the parameterized type: type Kl' s i o = i -> Kl1' s o data Kl1' s o = Kl1' (s -> (s,o)) compose' :: (Kl' s1 a b) -> (Kl' s2 b c) -> (Kl' (s1,s2) a c) But not with the quantified one: type Kl i o = i -> Kl1 o data Kl1 o = forall s. Kl1 (s -> (s,o)) compose :: (Kl a b) -> (Kl b c) -> (Kl a c) compose f1 f2 = \a -> Kl1 $ \(s1,s2) -> (f1 a) .> (\(Kl1 u1) -> (u1 s1) .> (\(s1', b) -> (f2 b) .> (\(Kl1 u2) -> (u2 s2) .> (\(s2', c) -> ((s1',s2'), c) )))) I guess this is the same question as before where the answer would be "move the quantifier back where it was", i.e. : data Kl i o = forall s. Kl1 (i -> s -> (s,o)) So maybe I should ask a different question: is there any reason why you can't make a Monad which has some state type that's hidden? Any way I try to write down the bind or join operations of a Monad instance for the type you suggested data Kl1 o = forall s. Kl1 (s -> (s,o)) I run into typing problems of the kind in compose above. I.e. for bind, the problem is of course almost exactly the same: bind :: (Kl1 i) -> (i -> Kl1 o) -> (Kl1 o) bind mi f = Kl1 $ \(s1,s2) -> mi .> (\(Kl1 u1) -> (u1 s1) .> (\(s1', i) -> (f i) .> (\(Kl1 u2) -> (u2 s2) .> (\(s2', o) -> ((s1',s2'),o)))))

[Reply][About]

[<<][meta][>>][..]