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

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][>>][..]