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