Modal FRP for all: Functional reactive programming without space leaks in Haskel...
summary
A modal FRP language Ratus is implemented as a Haskell library plus a GHC plugin that enforces stricter typing: a later modality for time-shifted values and a box modality for stable (always-available) data. The compiler runs a multi-tick → single-tick transform, desugars to a strict core, and proves causality, absence of space leaks and productivity via a Lambda-tick core formalized in Coq. Ships with an FRP library and a Pong example; installable with cabal.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:42Modal FRP
- 1:50Streams
- 3:34Model types
- 5:15Shallow embedding
- 7:23Ratus
- 8:40How Rus looks like
- 9:44How it works
- 12:47Memory leaks
- 15:44Stable types
- 18:24Pong game
- 19:34Implementation
- 22:52Met Theory
- 23:40Operations semantics
- 25:09Other resources
- 26:38Conclusion
related talks
36mAsynchronous Reactive Programming with Modal Types in Haskell
29mWhat is Functional Reactive Programming?
31mThe Beauty and Elegance of Functional Reactive Animation
45mFunctional Reactive Programming in Elm
36mHow Functional Programming Can Make Life Easier
35mActors Design Patterns and Arrowised FRP
41mFunctional Programming for Pragmatists
36mConcrete Functional Programming
