Causality for Free! Parametricity Implies Causality for Functional Reactive Programs

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

• Alan Jeffrey, Bell Labs
• Monday 23 July 2012, 14:00-15:30
• Small lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

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 http://research.microsoft.com. 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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.