Lambda the Ultimate

A simple model of programs in an FRP style is "newtype Putter a b = Putter (a -> (b, Putter a b))".
Unfortunately this doesn't model programs which can change the type of input and output they have.

I tried using GADT's to fix this and got

data PushAndPull i o where
 PushAndPull :: i o2 -> (o i2, PushAndPull i2 o2)

but it doesn't type check. Instead I can only have

data Pusher i o where
 Pusher :: i -> (o u, Pusher u o)

and

data Puller i o where
 Puller :: i u -> (o, Puller i u)

Because I can't figure out a model which typechecks, I want to find out alternate FRP models of programs which can change the type of input and output they have. What work in FRP models programs which can change the type of output and input they have?

If one wants to iterate through all reachable states s1 from an initial state s0 in an imperative language (think of a chess board and a possible set of moves) one could do something like:

for i in 1..#changes {
    s1 := copy(s0)
    change(s1, i)
    // process s1
}

It is usually faster and less memory intensive to do the following instead:

for i in 1..#changes {
    change(s0, i) pushing undo data to the stack
    // process s0
    undo(s0) popping undo data from the stack
}

Are there general techniques for inferring the "undo data" that an operation should save, and possibly the corresponding undo operation?