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

Tue Aug 16 20:24:29 CEST 2011

The existential unpacking problem

I'm thinking, to all great problems the nuts & bolts solution is to
introduce state or sequentiality.  What about writing this in CPS?
Something to keep in the back of the head..

Anyway, the problem is that I can't use something like this:

   f' a = case (f a) of (SSM i0 io) -> (i0, u0)

because it doesn't infer properly.  I switched to CPS because I
somehow have this hunch that this would work.  However, the following
doesn't infer properly:

  ssmUnpack (SSM s0 u) k = k s0 u

Using -XRank2Types I was able to construct a type like this:

  ssmUnpack :: SSM i o -> (forall s. s -> ((s,i) -> (s,o)) -> r) -> r

So it looks like we're a bit closer.  Can the same trick be used in
non-CPS form?  Doesn't look like it, at least I can't make this work:

  ssmUnpack' :: SSM i o -> (forall s. (s, ((s,i) -> (s,o))))
  ssmUnpack' (SSM s0 u) = (s0, u)

So let's try the CPS version.  It looks like I have to dig very deep
because that value is only exposed on the inside of bind (if
primitive) or join.

Plan: write the _join in SigJoin.hs in using a CPS unpack function.

Detour: the above seems not so simple, so I'm trying first to implemnt
the Kleisli isomorphism which I've used in the definition of Monad in
terms of Arrow.

ssmKleisli :: (i -> SSM () o) -> SSM i o

However, writing out this function with non-CPS unpack already gives
rise to a seemingly serious problem: the initial state is not
accessible without having the output, and the SSM representation
requires it to be naked.

ssmKleisli :: (i -> SSM () o) -> SSM i o
ssmKleisli f = 
  let u (s,i) =
        let (s0, u) = unpack (f i)
            (s', o) = u (s, ())
        in
         (s', 0)
  in
   SSM <cant-get-at-s0> u

In short: the initial state is hidden behind the input, and I have to
invert that order when creating an SSM.  This looks like a dead end.
Can't go from Kleisli to Monad for this particular case.

So the only way out seems to be to make the _join use a CPS unpack
function.  First, write _join in direct let form, then perform partial
CPS conversion.


I get to something, but I get stuck at a typing issue which I think
has to do with multiple versions of unpack that are used with
different types.

-- PLAIN
_join' (i1, u1) = ((i1, i2), u12) where
  (_, (i2, _)) = u1 i1 -- (**) 
  u12 (s1, s2) = ((s1', s2'), a) where
    (s1', (_, u2)) = u1 s1
    (s2', a)       = u2 s2

-- LET
_join mm =
  let unpack = \x -> x 
      (i1, u1) = unpack mm   -- unpack the double wrapper
      (_, m)   = u1 i1       -- use initial input to expose single wrapper
      (i2, _)  = unpack m    -- unpack it to get at initial state
      u12 (s1, s2) = 
        let (s1', m) = u1 s1    -- use current input to expose single wrapper
            (_, u2)  = unpack m -- unpack it to get at update function
            (s2', a) = u2 s2    -- run update
        in
         ((s1', s2'), a)
  in ((i1, i2), u12)

-- CPS
_joinCPS unpack mm =
  unpack mm 
  (\ (i1, u1) ->
    let (_, m) = u1 i1
    in unpack m 
       (\(i2, _) ->
         ((i1, i2),
          (\(s1, s2) ->
            let (s1', m) = u1 s1
            in unpack m 
               (\(_, u2) ->
                 let (s2',a) = u2 s2
                 in ((s1, s2'), a))))))


type Unpack w s a r = w -> ((Sig s a) -> r) -> r
_joinCPS :: (Unpack w' s a' r) -> w -> Sig (s1,s2) a

unpackTuple (i,u) k = k (i,u)


Bottom line: I can't seem to find a single spot to modify without
creating a huge unreadable expression that I can't type...

I'm done.

[Reply][About]

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