University of Cambridge > > Microsoft Research Cambridge, public talks > Causality for Free! Parametricity Implies Causality for Functional Reactive Programs

Causality for Free! Parametricity Implies Causality for Functional Reactive Programs

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

Functional Reactive Programming (FRP) is a model of reactive systems in which signals are time-dependent values, and signal functions are functions between signals. Signal functions are required to be causal, in that output behaviour at time t is only allowed to depend on input behaviour up to time t. In order to enforce causality, many FRP libraries are arrowized, in that they provide combinators for building signal functions, rather than allowing users to write functions directly. In this paper, we provide a definition of deep causality (which coincides with the usual definition on signals of base type, but differs on nested signals). We show that FRP types can be interpreted in System Fω extended with a kind of time, and show that in this interpretation, a “theorems for free” argument shows that parametric functions are deep causal. Since all System Fω functions are parametric, this implies that all implementable functions are deep causal. This model is the formal basis of the agda-frp-js FRP library for the dependently typed programming language Agda, which compiles to JavaScript and executes in the browser. Assuming parametricity of Agda, this allows reactive programs to be written as regular functions over signals, without sacrificing causality. All results have been mechanically verified in Agda.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity