Transcript FRP for Real - Computer Science

FRP for Real
Paul Hudak
Yale University
Department of Computer Science
April 2001
Joint work with:
Zhanyong Wan
Walid Taha
FRP




Fran is a DSL for graphics and animation.
Frob is a DSL for robotics.
FranTk is a DSL for graphical user interfaces.
FRP (functional reactive programming) is the
essence of Fran, Frob, and FranTk:



Fran = FRP + graphics engine + library
Frob = FRP + robot controller + library
FranTk = FRP + Tk substrate + library
 FRP has two key abstractions:


Continuous time-varying behaviors.
Discrete streams of events.
Domain-Specific Languages
FVision
FranTk
Frob
Fran
Graphics, Robotics, GUIs, Vision
FRP
Functional Programming
Applications
Specialized languages
Continuous behaviors
and discrete reactivity
Functions, types, etc.
(Haskell)
Behaviors
 Continuous behaviors capture any time-varying
quantity, whether:



input (sonar, temperature, video, etc.),
output (actuator voltage, velocity vector, etc.), or
intermediate values internal to a program.
 Operations on behaviors include:


Generic operations such as arithmetic, integration,
differentiation, and time-transformation.
Domain-specific operations such as edge-detection and
filtering for vision, scaling and rotation for animation and
graphics, etc.
Events
 Discrete event streams include user input as well as
domain-specific sensors, asynchronous messages,
interrupts, etc.
 They also include tests for dynamic constraints on
behaviors (temperature too high, level too low, etc.)
 Operations on event streams include:


Mapping, filtering, reduction, etc.
Reactive behavior modification (next slide).
Reactive Control of Continuous Values
One animation example that demonstrates
key aspects of FRP:
growFlower = stretch size flower
where size = 1 + integral bSign
bSign =
0 `until`
(lbp ==> -1 `until` lbr ==> bSign) .|.
(rbp ==> 1 `until` rbr ==> bSign)
Frob
 Recall that:
Frob = FRP + robot controller + robot/vision library
 Programming robots is a lot like programming an
animation!
 … except that:





The robot doesn’t always do what you want it to do.
Error / anomalous conditions are more common.
Real-time issues are more dominant.
Sensor input is critically important, but unreliable.
Robots have different response characteristics:


Often must react more quickly.
Often are slower than graphics hardware.
Robots with Vision
Nomadic Technologies SuperScout
(our old robots)
Vision
16 Sonars
Bumpers
Wheel
Controls
Computing:
PC running Linux
Hugs
Radio Modem
Autonomous Coordinated Motion
 Natural behavior amongst living animals:

flocking, herding, schooling, swarming
 Specific tasks of interest to us:

congregation, navigation, “escortation”,
formation motion, obstacle avoidance,
dispersion, etc.
 Key technologies of interest:


computational vision and control
FRP
Example of Coordinated Motion
 Problem:

Specify local control strategy for two differential-drive
robots in interleaving trajectories, where each robot only
knows the relative position of the other.
 Can be achieved by two-step simplification:


Non-holonomic constraint on differential-drive robot is
eliminated by considering a moving frame of reference.
Relative to that frame, each robot exhibits identical
behavior: simply circle the other robot.
 Frob permits abstract formulation of solution.


Two independent critically-damped PI controllers.
Local motion assumes holonomic vehicle; i.e. differential
drive robot can be treated as omni-directional robot.
Local Behavior
vFrame
desired rotation
vLat
vRot
moving
frame of
reference
Code Snippet
interleaveC dist omega0 vFrame =
let …
distError = distOther - dist
vLat = vector2Polar
(kpDist * distError +
kiDist * integralB distError)
angOther
vRot = vector2Polar
(omega0*distOther/2)
(angOther - pi/2)
in velocityV (vFrame + vLat + vRot)
History of FRP Research











TBag, Active VRML: Conal Elliott, ’95-97.
Fran: Elliott & Hudak, ICFP ’97.
Various implementations: Eliiott, DSL ’97, PLILP ’99.
Semantics: Anthony Daniels, PhD Thesis ‘99.
Frob: Peterson, Hager, Hudak, Elliott, ICRA ‘99, PADL ’99.
Used in robotics course at Yale in ‘99, ‘01.
Fvision: Peterson, Hager, Hudak, Reid, ICSE ’99, PADL ’01.
SOE’s “FAL”: Hudak, stream-based implementation of Fran-like
language, ’00.
FranTk: Fran-based GUI, Meurig Sage, ICFP ’00.
Frappé: Java-based FRP, Antony Courtney, PADL ’01.
Yale FRP: core language + growing library of graphics, robotics,
simulator, etc. code, ’00-01 (public release planned soon).
Semantics: Wan, Hudak, PLDI ’00, showed correspondence of
denotational and operational semantics.
Real-Time FRP
 How do we make FRP run fast?
 How do we make guarantees about both time and
space behavior?
 How does FRP relate to other models of hybrid
automata?
 Can FRP be used for embedded systems?
 And at a more abstract level:
What is an operational semantics for FRP?
Our goal:
Real-Time FRP, an abstract, restricted subset
of FRP, with guaranteed bounds on execution
time and space, and deadlock free.
Syntax of RT-FRP
 Syntax of lambda terms:
(“lifted” terms are just “Maybe” type)
 Syntax of values:
 Syntax of signals:
Note: “Event a” in FRP is isomorphic to “Behavior (Maybe a)”.
In RT-FRP we just combine them and call them “signals”.
Types
 Syntax of types:
 Contexts:
 Judgments:
“e is a functional term of type g”
“s is a signal carrying values of type g”
Or in Haskell: e :: g, and s :: Behavior g
Some Typing Rules
More typing rules
 Reactivity:
 Non-recursive binding:
 Recursive binding:
 Note:
let signal x = s in ext x == s
Recursion
 There are two “prototypical” kinds of recursion in FRP:
(1)
(2)
 Using recursive signals these can be expressed as:
(1)
(2)
But what about integral?
 Define using a delay in a recursive signal.
 By way of example, here is the running maximum of
a signal:
Definition of Integral
… using the forward Euler method:
From FRP to RT-FRP
and more…
Operational Semantics
 A program is executed in discrete steps, driven by
time-stamped input values.
 Given a time t and input i, a term s evaluates to a
value v and transitions to a new term s’.
 We write this as:
and
or, more compactly as:
where:
Program Execution
 A proper RT-FRP program never terminates.
Its meaning is the infinite sequence of values, or
“observations” that it yields.
 The sequence:
t0,i0
t1,i1
t2,i2
s0  s1,v1 ; s1  s2,v2 ; s2  s3,v3 ; …
is abbreviated:
t0,i0
t1,i1
t2,i2
s0  v1, s1  v2, s2  v3, s3 …
 Meta-comment: Program meaning depends on the
time-stamped input pairs (tj,ij).
Some Eval Rules
More Eval Rules
(ev-signal)
Some Transition Rules
More Transition Rules
and more…
(tr-switch-noc)
(tr-switch-occ)
Tail Signals
 Recursive signals are nice, but we’d like something
better:
 With let-continuation, we can define tail-recursive
signals that can also pass values.
 Similar to standard model of hybrid automata.
 Note: the syntax prevents unbounded term growth
as in: letcont k x = s0 until x=ev then k x + 1
not possible
For Example
 A simple model of a thermostat:
let signal temp =
let cont k1 () = <heating-model>
until when (temp>t) => k2
k2 () = <cooling-model>
until when (temp<t-hys) => k1
in t0 until startev => k1
in ext temp
Key Results

Type safety / preservation


Each step takes constant time


thus no time leaks!
Term size cannot grow


thus no core dumps!
thus no space leaks!
In addition, with a notion of well-formed
recursion, progress is guaranteed.

thus no deadlock!
Preventing Deadlock
 FRP programs are naturally “infinite” – signals are streams of
values with unbounded extent. This is a good thing!
 With recursion, however, terms can become “stuck”:

let signal x = ext x in ext x
 Solution: define notion of well-formed recursion that disallows
“direct” recursions, and thus prevents deadlock.
 Key idea: in “let signal x = s1 in s2”, we require that s1 is in
W{x}, where:
Wx = input | time | ext e where e contains no X |
delay v s | let signal y = Wx in Wx |
Wx switch on x = ev in Wx | …
 In other words, a delay must appear somewhere.
Future Work on RT-FRP






Enrich language for practical use.
Compile into lower-level code (C, etc.).
Examine sensor / behavior fusion.
Consider embedded systems.
Better formulation of well-formed recursion.
Test case: compile to PIC microcontroller on
our “soccer-bots”.
How to Hide a Flock of Turkeys