What work in FRP models programs which can change the type of output and input they have?

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?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Type as a function of what?

If the type for the next `Putter` program is a function of the argument `a`, then you'd need dependent typing, which is beyond Haskell's expressiveness.

If the type for the next `Putter` program is a simplistic function of the current types, you could probably use type families. But I think this would only work well if you had simple cyclic types (a, b, c, a, b, c, ...). Even then it might be difficult to compose.

If you just need flexible types for IO, consider use of Data.Typeable and the work on Cloud Haskell.

Session Types

I don't think you're describing FRP at all, but just stream processing with a Mealy automaton. That said, what you're describing an interest in seems to be session-typed coroutines, like so.

Sigfpe also has a neat little simple version on his blog.