infinite types
blaat blaat
l4t3r@hotmail.com
Fri, 18 Jul 2003 01:30:18 +0200
Uhm, of to my holliday in France. But, ah, oh, the joy of programming ;-). I
thought I would humor this list by showing where the infinite types (is it?)
discussion ended. I found it quite nice and the code is short so here goes
;-)
To test: save the mail after the marker and run it in Hugs. There are some
examples at the end of the file.
------- cut from here, save as "Reactive.hs"
---------------------------------
-- A reactive system is modelled by the type
--
-- R m = m -> (Nottaken | Taken (R m) [m])
--
-- It is _not_ a coalgebraic definition, it is _not_ an arrow, it is
-- a recursive type in this case used to model asynchronous message
-- passing systems.
--
-- A system may be thought of as collection of (UML)
-- transitions: s0 - event[guard]/action* -> s1 where states are
-- hidden in the transitions, and a next-state is a transition,
-- or something, I guess. Uhm, huh? ;-)
--
-- Note that no explicit distinction between in- and output messages
-- is made. This allows liberal, although slightly odd ;-), structural
-- composition operators a la Broy, Bird-Meertens, Arrows, Fudgets,
-- whatever. In a nutshell: stream processing functions.
--
-- After reading the following oddball operators, you, uhm, might
-- really want to define your own. Really ;-)
--
-- This formalization has weak algebraic rules on the composition
-- operators.
--
-- Load this code in hugs and test the examples by typing ex0 to
-- ex6.
module Reactive where
type R m = m -> Response m
data Response m = Nottaken | Taken (R m) [m]
----------------------------------------------------------------------
--
-- onTaken: helper function
onTaken::Response m -> (R m -> [m] -> a) -> a -> a
onTaken Nottaken f g = g
onTaken (Taken s oo) f g = f s oo
----------------------------------------------------------------------
--
-- The behavior of a system is, of course, a mapping from an input
-- stream of messages to an output stream of messages.
behavior::R m->[m]->[m]
behavior s [] = []
behavior s (i:ii) = onTaken (s i)
(\s0 oo-> oo ++ behavior s0 ii)
(i:behavior s ii)
----------------------------------------------------------------------
-- Copy is a simple system which copies all input to its output.
--
-- +++++
-- + +
-- +++++
----------------------------------------------------------------------
copy::R m
copy m = Taken copy [m]
----------------------------------------------------------------------
-- Lift is a simple system which is the lifting of a function from
-- messages to messages to a reactive system.
--
-- +++++++++
-- + ^ +
-- + f +
-- + +
-- +++++++++
----------------------------------------------------------------------
lift::(m->m) -> R m
lift f m = Taken (lift f) [f m]
----------------------------------------------------------------------
--
-- If we have a system on messages of type b, and translator functions
-- between another type a, we can change the interface to a system
-- on messages of type a. (This is a solution for not
-- making an explicit distinction between input and output messages;
-- now we can partition the messages of subsystems)
--
-- +++++++++
-- + +
-- + s:R a +:R b
-- + +
-- +++++++++
interface::(a->b)->(b->a)->R b->R a
interface t f s i = onTaken (s (t i))
(\s1 oo->Taken (interface t f s1) (map f oo))
(Nottaken)
----------------------------------------------------------------------
--
-- The parallel composition of two systems s and r is the system which
-- if s takes an input then makes s process it, otherwise if r takes an
-- input then makes r process it, otherwise does not process it.
--
-- Supposed to model the parallel composition of a collection of
-- event handlers (like: sound subsystem, graphics subsystem, etc).
--
-- +++++
-- + s +
-- + + +
-- + r +
-- +++++
--
-- ( (a <+> b) <+> c = a <+> (b <+> c) )
parallel::R m->R m->R m
parallel s0 s1 i = onTaken (s0 i)
(\s2 oo->Taken (parallel s2 s1) oo)
(onTaken (s1 i)
(\s2 oo->Taken (parallel s0 s2) oo)
(Nottaken))
infixr 5 <+>
(<+>) = parallel
----------------------------------------------------------------------
--
-- The sequential composition of systems s and r takes an input if
-- s accepts the input and then makes r process all output of s.
-- All output by s which is not taken by r _passes through_ r.
--
-- Supposed to model pipes (where exceptions or messages to the
-- outside world leak through).
--
--
-- +++++++
-- + s.r +
-- +++++++
--
-- ( (a <.> b) <.> c = a <.> (b <.> c) )
--
sequential::R m->R m->R m
sequential s0 s1 i = onTaken (s0 i)
(\s2 oo->
onTaken (seqloop s1 oo)
(\s3 oo1->
(Taken (sequential s2 s3) oo1))
(Nottaken))
(Nottaken)
seqloop::R m->[m]->Response m
seqloop s [] = Taken s []
seqloop s (i:ii) = onTaken (s i)
(\s1 oo0->
onTaken (seqloop s1 ii)
(\s2 oo1 -> Taken s2 (oo0++oo1))
(Nottaken))
(onTaken (seqloop s ii)
(\s1 oo -> Taken s1 (i:oo))
(Nottaken))
infix 6 <.>
(<.>) = sequential
----------------------------------------------------------------------
--
-- Feedback on a system s feeds _all_ output of s back to s. All
-- output which is not accepted by s _passes through_ s (and the
-- loop).
--
-- Feedback folds all the transitions taken over fed back output
-- into _one_ big transition...
--
-- +++++
-- -+-++ s +-+--
-- | +++++ ^
-- +--------+
----------------------------------------------------------------------
feedback::R m->R m
feedback s i = onTaken (s i)
(\s0 oo0-> onTaken (feedloop s0 oo0)
(\s1 oo1-> Taken (feedback s1) (oo1))
(Nottaken))
(Nottaken)
feedloop::R m->[m]->Response m
feedloop s [] = Taken s []
feedloop s (i:ii) = onTaken (s i)
(\s0 oo-> feedloop s0 (ii++oo))
(onTaken (feedloop s ii)
(\s0 oo -> Taken s0 (i:oo))
(Nottaken))
feed = feedback
----------------------------------------------------------------------
-- small examples:
----------------------------------------------------------------------
test s = take 40 (behavior s (repeat 1))
ex0 = test copy
ex1 = test (lift (*2) <.> lift ((-)1))
ex2 = test (lift (+1) <+> lift (*2))
ex3 = test (lift (+2) <+> copy <.> lift (+3))
ex4 = test (feed copy) -- infinite computation
ex5 = test (interface (\i->'a') (\a->5) copy)
----------------------------------------------------------------------
-- bigger example:
----------------------------------------------------------------------
data Msg = Tick | Out Int
| Add Int | AddResult Int
| Write Int Int | Fetch Int | Read Int Int
deriving (Show)
add::Maybe Int -> R Msg
add Nothing (Add j) = Taken (add (Just j)) []
add (Just i) (Add j) = Taken (add Nothing ) [AddResult (i+j)]
add _ _ = Nottaken
register::Int->Int->R Msg
register i _ (Write j r) | i == j = Taken (register i r) []
register i r (Fetch j) | i == j = Taken (register i r) [Read i r]
register _ _ _ = Nottaken
controller::R Msg
controller Tick = Taken controller [Fetch 0, Fetch 1]
controller (Read i j) = Taken controller [Add j, Write (1-i) j]
controller (AddResult i) = Taken controller [Out i, Write 1 i]
controller _ = Nottaken
ex6 = test
(interface (\_->Tick) (\(Out i)-> i)
(feed (register 0 0<+>register 1 1<+>add Nothing<+>controller)))
----------------------------------------------------------------------
-- This code is licensed under the Big-Kazooba-Ritual license:
--
-- You may copy, modify or distribute this software provided that
-- you first perform the ritual described in section a.
--
-- If you ever meet one of the authors of this work you can be asked,
-- and must comply, to perform the ritual as described in section a.
--
-- You must add this license to any derivatives of this work.
--
-- a. Lift your left leg, close your eyes and jump in the air.
-- Now tap the point of your nose exactly two times with your
-- right index finger. To complete: say the words
-- "thank you Big Kazooba"
--
-- You may open your eyes now.
--
-- The disabled may opt not to perform this ritual but have a
-- volunteer perform the ritual on their behalf.
--
-- Anyone, of suited position, may opt to command any number of
-- subordinates to perform the ritual instead.
--
-- Thank you,
-- l4t3r
----------------------------------------------------------------------
_________________________________________________________________
MSN 8 helps eliminate e-mail viruses. Get 2 months FREE*.
http://join.msn.com/?page=features/virus