[<<][meta][>>][..]
Sat Aug 20 20:11:59 CEST 2011
Answer to Oleg's post
( 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][>>][..]