Went back and watched two of the Little Languages 2 Workshop presentations. Specifically Joe Armstrong and Todd Proebsting's presentations on "Concurrency Orientated Programming", and "Disruptive Programming Language Technologies" respectively. I highly recommend both these talks to anyone who is the slightest bit interested in programming languages, or has any serious involvement in development. It is just unfortunate that they are only available as real-video. Still if you have r-v installed, they are both well worth the time.
Tuesday, November 23, 2004
Andrew Newman came across this set of articles on OO theory. I stumbled across them about a year ago, read the first few, changed jobs, and promptly forgot to go find them again. I remember them as well worth the time to read.
This is the first article in a regular series on object-oriented type theory, aimed specifically at non-theoreticians. The object-oriented notion of classification has for long been a fascinating issue for type theory, chiefly because no other programming paradigm has so sought to establish systematic sets of relationships between all of its types. Over the series, we shall seek to find answers to questions such as: What is the difference between a type and a class? What do we mean by the the notion of plug-in compatibility? What is the difference between subtyping and subclassing? Can we explain inheritance, method combination and template instantiation? Along the way, we shall survey a number of different historical approaches, such as subtyping, F-bounds, matching and state machines and seek to show how these models explain the differences in the behaviour of popular object-oriented languages such as Java, C++, Smalltalk and Eiffel. The series is titled "The Theory of Classification", because we believe that all of these concepts can be united in a single theoretical model, demonstrating that the object-oriented notion of class is a first-class mathematical concept!Anyway, the links:
"The Theory of Classification"1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, and 15.
Monday, November 15, 2004
Just noting that I have updated the Arrows 'n Robots summary with links to citeseer and Wan's thesis page on the Yale-group pages. Also wanted to dump the url to the Yale group here so next time I can find it more easily.
I have had a few people ask me to explain the utility and signifigance of category theory. This proves rather difficult given I am a complete novice in this area myself; desprately trying to keep my head above water in the simplest of papers. Still I found this paragraph useful, and I decided to post it here so I can find it again.
Category theory unifies mathematical structures in a second, perhaps even more important, manner. Once a type of structure has been defined, it quickly becomes imperative to determine how new structures can be constructed out of the given one and how given structures can be decomposed into more elementary substructures. For instance, given two sets A and B, set theory allows us to construct their cartesian product A X B. For an example of the second sort, given a finite abelian group, it can be decomposed into a product of some of its subgroups. In both cases, it is necessary to know how structures of a certain kind combine. The nature of these combinations might appear to be considerably different when looked at from too close. Category theory reveals that many of these constructions are in fact special cases of objects in a category with what is called a "universal property". Indeed, from a categorical point of view, a set-theoretical cartesian product, a direct product of groups, a direct product of abelian groups, a product of topological spaces and a conjunction of propositions in a deductive system are all instances of a categorical concept: the categorical product. What characterizes the latter is a universal property. Formally, a product for two objects a and b in a category C is an object c of C together with two morphisms, called the projections, p: c → a and q: c → b such that, and this is the universal property, for all object d with morphisms f: d → a and g: d → b, there is a unique morphism h: d → c such that p o h = f and q o h = g. Notice that we have defined a product for a and b and not the product for a and b. Indeed, products and, in fact, every object with a universal property, are defined up to (a unique) isomorphism. Thus, in category theory, the nature of the elements constituting a certain construction is irrelevant. What matters is the way an object is related to the other objects of the category, that is, the morphisms going in and the morphisms going out, or, put differently, how certain structures can be mapped into it and how it can map its structure into other structures of the same kind.Jean-Pierre Marquis, Stanford Encyclopedia of Philosophy: Category Theory
Friday, November 12, 2004
First some background reading from the bibliography I'll have to read eventually:
- John Hughes. Generalising monads to arrows. Science of Computer Programming, 37:67-111, May 2000
- Ross Paterson. A Notation for Arrow-based Libraries. In ICFP'01: International Conference on Functional Programming, pages 229-240, Firenze, Italy, 2001
- Zhanyong Wan. Functional Reactive Programming for Real-Time Embedded Systems. PhD thesis, Department of Computer Science, Yale University, December 2002
- Zhanyong Wan, Walid Taha, and Paul Hudak. Real-time FRP. In Proceedings of Sixth ACM SIGPLAN '00 Conference on Programming Language Design and Implementation (PLDI), pages 242-252, Vancouver, BC, Canada, June 2000. ACM, ACM Press.
- Zhanyong Wan, Walid Taha, and Paul Hudak. Event-driven FRP. In Proceedings of Fourth International Symposium on Practical Aspects of Declarative Languages. ACM, Jan 2002
Naturally when you are using FRP the core concept is that of the signal. So we define signal to have the type
Signal a = Time -> a, ie a function of Time returning a value of type 'a'; s(t). The robot used throughout the paper is a simple differential drive with a handful of basic sensors. So given two signals vr(t) ->
vr::Signal Double and vl(t)
vl::Signal Double which are the velocities of the right and left wheels respectively we can write an reactive program for calculating the robots position:
x = (1 / 2) * integral ((vr + vl) * sin theta) y = (1 / 2) * integral ((vr + vl) * cos theta) theta = (1 / l) * integral (vr - vl)Of course the nice thing about this program is that it is a direct transliteration of the physics equations governing the motion of such a robot! This is why FRP is important.
Such programs are clear, consise, correct, and unfortunately completely unworkable in the general case. The problem is that while in the small (with simple toy examples) you couldn't get better than this, larger programs tend to lead to opaque space and time management with the resultant space and time leaks. The focus on this paper is how to retain most of the legibility and good domain match of FRP while preventing leaks. The FRP DSL developed in this paper is called Yampa, and it solves the leak problem by disallowing signals as first class values. Instead signals are manipulated indirectly via set of combinators called signal transformers or signal functions.
SF a b = Signal a -> Signal bThis of course is very similar to the Haskell IO or State monads, and reminisent of Hutton's Monadic Parser Combinators. On the other hand, as presaged by the subject, the authors use Arrows rather than Monads as the basis for their combinator library.
A good analogy for this idea is a state or IO monad, where the state is hidden, and a program consists of a linear sequencing of actions that are eventually run by an interpreter or the operating system. But in fact arrows are more general than monads, and in particular the composition of signal functions does not have to be completely linearSpecifically Arrow contains a fixedpoint combinator
loopwhich provides access to recursion.
The basic combinators include.
- lift function:
arr :: ( a -> b ) -> SF a b
- Takes a normal function from type 'a' to 'b', and returns a signal-function/transformer that will convert a signal of type 'Signal a' to 'Signal b'.
(>>>) :: SF a b -> SF b c -> SF a c
- Takes two signal functions and returns the composition of them
(&&&) :: SF a b -> SF a c -> SF a (b, c)
- This permits you to take one signal and apply two functions to it similtaniously producing two signals both independently derived from the input. And of course, once you have tupled outputs....
(***) :: SF a b -> SF c d -> SF (a c) (b d)
- Take two signal functions and returns a transformer that applies them to the respective signals in a tupled signal.
Some standard combinators provided:
So now convert the original FRP expression for x(t) to raw arrow-form:
x = (1/2) * integral ((vr + vl) * cos theta) given: vrSF :: SF RobotInput Velocity (SF that extracts vr from a RobotInput) and vlSF :: SF RobotInput Velocity (SF that extracts vl from a RobotInput) and thetaSF :: SF RobotInput Angle xSF :: SF RobotInput Distance -- Signal Function transforming RobotInput -> Distance xSF = (((vrSF && vlSF) >>> arr2 (+)) &&& (thetaSF >>> arr cos)) >>> arr2 (*) >>> integral >>> arr (/2) or slightly more legible: xSF = let v = (vrSF &&& vlSF) >>> arr2 (+) t = thetaSF >>> arr cos in (v &&& t) >>> arr2 (*) >>> integral >>> arr (/2) which isn't all that much better.So what we have gained above is the ability to mediate access to signals behind a reasonably safe, yet complete abstraction. However the loss in clarity is striking. Fortunately there is a proposed arrow-syntax that is similar to Haskell's monadic do-syntax.
xSF' :: SF RobotInput Distance xSF' = proc inp -> do vr <- vrSF -< inp vl <- vlSF -< inp theta <- thetaSF -< inp i <- integral -< (vr + vl) * cos theta returnA -< (i / 2)Which while not as nice as the original FRP, has the triple advantage of being declarative, legible, and safe!
It is important to note that the arrow syntax allows one to get a handle on a signal's values (or samples), but not on the signals themselves. In other words, first recalling that a signal functionAlthough I can't reproduce it here, Fig 2 is dramatic. The correspondance between arrow-based signal-functions, and the signal-flow-diagrams shown is striking, and exciting. I have been excited about the potential of FRP to liberate UI programming from the tyranny of the state-machine; Fig 2 amazed at the clarity available. I am now, more than ever, convinced that I am on the right track.
SF acan be thought of as a type
Signal a -> Signal b, which in turn can be thought of as type
(Time -> a) -> (Time -> b), the syntax allows getting a handle on values of type
b, but not on values of type
Time -> aor
Time -> b.
Events diverge from Signals slightly in that while they are also temporal values, event's don't so much change from one value to another over time, as simply not exist between 'impulses' (in the signal processing sense). In fact their is an isomorphism between impulse-streams vs. continuous-signals and event-streams vs. signals. In previous papers the authors accepted this distinction as signifigant, and the two were treated seperately. However by noting an isomorphism between
Event a and
Maybe a they are able to define a signal of type
Signal (Event b) ie. an event stream, which becomes a signal that can be thought of as alternating between
Just a. A signal function of type
SF a (Event b) generates an event stream, and is called an event source.
There are a number of combinators for use with event-streams. I'm just going to list them with minimal discussion, for more than that see the paper.
switch, dSwitch :: SF a (b, Event c) -> (c -> SF a b) -> SF a b -- switch or delayed-switch. Note the function from the event payload to a new SF a b. rSwitch, drSwitch :: SF a b -> SF (a, Event (SF a b)) b -- note event is defined to carry an SF (possibly inserted by tag), this allows for recurring switch. tag :: Event a -> b -> Event b mergeBy :: (a -> a -> a) -> Event a -> Event a -> Event a lMerge, rMerge :: Event a -> Event a -> Event a -- Different ways of handing event collision. -- Useful event-sources: edge :: SF Bool (Event ()) -- Obtain an edge trigged event-stream from a (Signal Boolean) never :: SF a (Event b) now :: b -> SF a (Event b) after :: Time -> b -> SF a (Event b) repeatably :: Time -> b -> SF a (Event b) -- Useful event-stream transform back to signal space: hold :: a -> SF (Event a) a accum :: a -> SF (Event (a -> a)) (Event a) accumHold :: a -> SF (Event (a -> a)) a accumHold init = accum init >>> hold init
Finally just to show how it goes together, the paper implements a few robot controllers. First you implement your robot's controller as a signal function from RobotInput to RobotOutput. So a FRP mapping from the robots sensor-signals to signals which the signal-function-processor will apply to the robot's actuators. This controller is actually parametised by the robots properties, but that isn't surprising:
type RobotController = RobotProperties -> SF RobotInput RobotOutput.Finally the FRP engine is implemented as a function from a controller to IO(). In the case of the RobotSimulator implemented for the paper, the engine also takes a second controller and a world description.
runSim :: Maybe WorldTemplate -> RobotController -> RobotController -> IO ()Of course, returning the IO monad, this can be trivially instansated as as Haskell main function.
All in all a fascinating paper --- well worth the time to read.
Thursday, November 11, 2004
Now this is a fun paper. I mean, Category Theory, FRP, and you get to play with Robots! What more could you want? So lets take these three elements individually, and then I will try and summarise the paper.
- Category Theory
- My understanding of Category Theory is as a systematic treatment of abstraction and generalisation. It allows us to take collections of mathmatical proofs and theorms that have the same structure/form, abstract them into a categorical notation, and then generalise them by providing mappings from the categorial constructs to concepts in specific domains. This is naturally of signifigant interest to type-theorists who treat programs as proofs and want access to the power of parametic/polymorphic types and functions without sacrificing rigor. Arrows are a concept from category theory, a generalisation of Monads which beyond just lifting sequencing to a first-class object, allow parametised composition of sequencing. This gives us the ability to support the more complex temporal sequencing of operations required by...
- Functional Reactive Programming
- Or as that is a bit of a mouthful, FRP; is one of the most intuitive and widespread programming paradigms in use today. It is an approach to programming that has been made so unobtrusive that four of the five other members of my family use it (in the form of a spreadsheet) without realising they are programming. At a basic level, FRP introduces a new paramatised datatype into the language, the time-varying 'signal'. By then permitting functions to be defined that accept these signals and return time-varying signals, you eliminate the shared-state, duplicated-logic, fragmented code paths, and explicit state-machines spawned by current, traditional event-driven approaches. As a basis for comparison, just imagine comparing a traditional spreadsheet with one where to implement a formula for a cell you would have to attach an 'onChange' callback to each referenced cell that recalculated the value.
- Robots have a number of constraints that have not been traditionally considered strengths of functional programming.
- Large numbers of discrete and continuous time-varying inputs that are most definately *note* referentially transparent.
- Real-time constraints that impose a requirement to avoid time-leaks, which encourages the use of imperative operation sequences. Execution of which can be easilly suspended and resumed as higher priority tasks require resources.
- Extensive use of embedded controllers and limited compuational resources that place a premium on transparency of resource use and strict avoidance of space-leaks.
- A history of research largely based on low level system languages (ie MIML) and assembly, which makes for a hostile reception for many of the assumptions of higher-level functional programming
Finished the Bananas and Lenses paper on the weekend, along with another on FRP that I'll summarise later. Section 4 takes the previous work based on Lists from section 2 and combines it with the category-theory results from section 3 to develop a theory of cata/ana/hylo/para -morphisms over arbitary datatypes. Section 5 is a very brief extension to parametric types.
Unfortunately I simply don't have enough category theory to follow the discussion properly, let alone explain it here. I think it is probably time to make another visit to Amazon and pick up a book or two on category theory. I'm thinking probably Pierce's introduction, and possibly Crole's "Categories for Types" on the basis of the review there. I've already read Pierce's intro, and it is mercifully brief and yet even from a quick reading I found I remembered enough to follow fragments of the paper. Unfortunately I found it too brief to allow me to learn enough to follow the rest :/.
Anyway, this paper was just for fun; fun was had; and I come away with a fresh perspective on recursion. That counts as a win for me.