Home

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" :-)

Guarded Induction and Weakly Final Coalgebras in Dependent Type Theory

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.
By Andris Birkmanis at 2005-08-08 11:18 | Type Theory | other blogs | 12940 reads

Comment viewing options

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

Backlink

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.

By Andris Birkmanis at Mon, 2005-08-08 11:34 | login or register to post comments

A less-annoying resumption monad

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))

instance Monad m => Monad (ReactT r m) where
    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)
By Dave Menendez at Mon, 2005-08-08 15:59 | login or register to post comments

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.

By Andris Birkmanis at Mon, 2005-08-08 17:23 | login or register to post comments