## Guarded Induction and Weakly Final Coalgebras in Dependent Type Theory

Quite a mouthful, I wonder if it would attract more people if it were titled "Interactive programming in Epigram" :-)
In this article we are going to explore one approach to the representation of interactive programs in dependent type theory. The approach we take centres on the concept of "monadic IO" used in functional programming. We will see that in dependent type theory, besides non-dependent interactive programs in which the interface between the user and the real world is fixed, as in ordinary functional programming, there is a natural notion of state-dependent interactive programs, in which the interface changes over time.

## Comment viewing options

I found this paper as a result of searches triggered by trampoline papers. It annoyed me how all responses to all requests were lumped into a single type (e.g., page 14 of cheap threads). Well, it was obvious that I need dependent types. From that it was a single step to this paper. I am not sure I will use it in my job (after all, Java has no dependent types - and I hope Java 8.0 TM will not introduce them :-) ), but sometimes theoretical papers tend to clarify the chaos in my head (induced by practical hype articles).

Hope you enjoy this paper.

It annoyed me how all responses to all requests were lumped into a single type (e.g., page 14 of cheap threads).

That annoyed me too, so I worked out a variant where the type of the response is indexed in the type of the request. It requires rank-2 polymorphism, but it's otherwise pretty simple:


data ReactT r m a = D a | forall c. P (r c) (c -> m (ReactT r m a))

return = D

D x   >>= f = f x
P q r >>= f = P q (\c -> r c >>= \k -> return (k >>= f))

signal :: Monad m => r a -> ReactT r m a
signal q = P q (return . return)

class Signal r where cont :: r ()

instance (Signal r) => MonadTrans (ReactT r) where
lift m = P cont (\_ -> m >>= return . D)


### Simple indeed

And it covers the static case fully.

One wonders, whether dynamic signature of input/output (section 3) is worth trouble of bringing full dependent types into trenches?

Probably Epigram folks can tell.