Denotational design with type class morphisms

I’ve just finished a draft of a paper called Denotational design with type class morphisms, for submission to ICFP 2009. The paper is on a theme I’ve explored in several posts, which is semantics-based design, guided by type class morphisms.

I’d love to get some readings and feedback. Pointers to related work would be particularly appreciated, as well as what’s unclear and what could be cut. It’s an entire page over the limit, so I’ll have to do some trimming before submitting.

The abstract:

Type classes provide a mechanism for varied implementations of standard interfaces. Many of these interfaces are founded in mathematical tradition and so have regularity not only of types but also of properties (laws) that must hold. Types and properties give strong guidance to the library implementor, while leaving freedom as well. Some of the remaining freedom is in how the implementation works, and some is in what it accomplishes.

To give additional guidance to the what, without impinging on the how, this paper proposes a principle of type class morphisms (TCMs), which further refines the compositional style of denotational semantics. The TCM idea is simply that the instance’s meaning is the meaning’s instance. This principle determines the meaning of each type class instance, and hence defines correctness of implementation. In some cases, it also provides a systematic guide to implementation, and in some cases, valuable design feedback.

The paper is illustrated with several examples of type, meanings, and morphisms.

You can get the paper and see current errata here.

The submission deadline is March 2, so comments before then are most helpful to me.

Enjoy, and thanks!

3D rendering as functional reactive programming

I’ve been playing with a simple/general semantics for 3D. In the process, I was surprised to see that a key part of the semantics looks exactly like a key part of the semantics of functional reactivity as embodied in the library Reactive. A closer look revealed a closer connection still, as described in this post.

Continue reading ‘3D rendering as functional reactive programming’ »

Sequences, segments, and signals

The post Sequences, streams, and segments offered an answer to the the question of what’s missing in the following box:

infinitefinite
discreteStream Sequence
continuousFunction ???

I presented a simple type of function segments, whose representation contains a length (duration) and a function. This type implements most of the usual classes: Monoid, Functor, Zip, and Applicative, as well Comonad, but not Monad. It also implements a new type class, Segment, which generalizes the list functions length, take, and drop.

The function type is simple and useful in itself. I believe it can also serve as a semantic foundation for functional reactive programming (FRP), as I’ll explain in another post. However, the type has a serious performance problem that makes it impractical for some purposes, including as implementation of FRP.

Fortunately, we can solve the performance problem by adding a simple layer on top of function segments, to get what I’ll call “signals”. With this new layer, we have an efficient replacement for function segments that implements exactly the same interface with exactly the same semantics. Pleasantly, the class instances are defined fairly simply in terms of the corresponding instances on function segments.

You can download the code for this post.

Edits:

  • 2008-12-06: dup [] = [] near the end (was [mempty]).
  • 2008-12-09: Fixed take and drop default definitions (thanks to sclv) and added point-free variant.
  • 2008-12-18: Fixed appl, thanks to sclv.
  • 2011-08-18: Eliminated accidental emoticon in the definition of dup, thanks to anonymous.

Continue reading ‘Sequences, segments, and signals’ »

Sequences, streams, and segments

What kind of thing is a movie? Or a song? Or a trajectory from point A to point B? If you’re a computer programmer/programmee, you might say that such things are sequences of values (frames, audio samples, or spatial locations). I’d suggest that these discrete sequences are representations of something more essential, namely a flow of continuously time-varying values. Continuous models, whether in time or space, are often more compact, precise, adaptive, and composable than their discrete counterparts.

Functional programming offers great support for sequences of variable length. Lazy functional programming adds infinite sequences, often called streams, which allows for more elegant and modular programming.

Functional programming also has functions as first class values, and when the function’s domain is (conceptually) continuous, we get a continuous counterpart to infinite streams.

Streams, sequences, and functions are three corners of a square. Streams are discrete and infinite, sequences are discrete and finite, and functions-on-reals are continuous and infinite. The missing corner is continuous and finite, and that corner is the topic of this post.

infinitefinite
discreteStream Sequence
continuousFunction ???

You can download the code for this post.

Edits:

  • 2008-12-01: Added Segment.hs link.
  • 2008-12-01: Added Monoid instance for function segments.
  • 2008-12-01: Renamed constructor “DF” to “FS” (for “function segment”)
  • 2008-12-05: Tweaked the inequality in mappend on (t :-># a).

Continue reading ‘Sequences, streams, and segments’ »

Simplifying semantics with type class morphisms

When I first started playing with functional reactivity in Fran and its predecessors, I didn’t realize that much of the functionality of events and reactive behaviors could be packaged via standard type classes. Then Conor McBride & Ross Paterson introduced us to applicative functors, and I remembered using that pattern to reduce all of the lifting operators in Fran to just two, which correspond to pure and (< *>) in the Applicative class. So, in working on a new library for functional reactive programming (FRP), I thought I’d modernize the interface to use standard type classes as much as possible.

While spelling out a precise (denotational) semantics for the FRP instances of these classes, I noticed a lovely recurring pattern:

The meaning of each method corresponds to the same method for the meaning.

In this post, I’ll give some examples of this principle and muse a bit over its usefulness. For more details, see the paper Simply efficient functional reactivity. Another post will start exploring type class morphisms and type composition, and ask questions I’m wondering about.

Continue reading ‘Simplifying semantics with type class morphisms’ »

Simply efficient functional reactivity

I submitted a paper Simply efficient functional reactivity to ICFP 2008.

Abstract:

Functional reactive programming (FRP) has simple and powerful semantics, but has resisted efficient implementation. In particular, most past implementations have used demand-driven sampling, which accommodates FRP’s continuous time semantics and fits well with the nature of functional programming. Consequently, values are wastefully recomputed even when inputs don’t change, and reaction latency can be as high as the sampling period.

This paper presents a way to implement FRP that combines data- and demand-driven evaluation, in which values are recomputed only when necessary, and reactions are nearly instantaneous. The implementation is rooted in a new simple formulation of FRP and its semantics and so is easy to understand and reason about.

On the road to efficiency and simplicity, we’ll meet some old friends (monoids, functors, applicative functors, monads, morphisms, and improving values) and make some new friends (functional future values, reactive normal form, and concurrent “unambiguous choice”).

Functional reactive chatter-bots

In a few recent posts, I’ve been writing about a new basis for functional reactive programming (FRP), embodied in the Reactive library. In those posts, events and reactive values are (first class) values. A reactive system able to produce outputs from inputs might have type Event a -> Event b or perhaps Reactive a -> Reactive b.

Although I’m mostly happy with the simplicity and expressiveness of this new formulation, I’ve also been thinking about arrow-style formulations, as in Fruit and Yampa. Those systems expose signal functions in the programming interface, but relegate events and time-varying values (called “behaviors” in Fran and “signals” in Fruit and Yampa) to the semantics of signal functions.

If you’re not familiar with arrows in Haskell, you can find some getting-started information at the arrows page.

This post explores and presents a few arrow-friendly formulations of reactive systems.

Edits:

  • 2008-02-06: Cleaned up the prose a bit.
  • 2008-02-09: Simplified chatter-bot filtering.
  • 2008-02-09: Renamed for easier topic recognition (was “Invasion of the composable Mutant-Bots”).
  • 2008-02-10: Replaced comps by the simpler concatMB for sequential chatter-bot composition.

Continue reading ‘Functional reactive chatter-bots’ »

Future values via multi-threading

Future values

A previous post described future values (or simply “futures”), which are values depend on information from the future, e.g., from the real world. There I gave a simple denotational semantics for future values as time/value pairs. This post describes the multi-threaded implementation of futures in Reactive‘s Data.Reactive module.

Continue reading ‘Future values via multi-threading’ »

Future values

A future value (or simply “future”) is a value that might not be knowable until a later time, such as “the value of the next key you press”, or “the value of LambdaPix stock at noon next Monday” (both from the time you first read this sentence), or “how many tries it will take me to blow out all the candles on my next birthday cake”. Unlike an imperative computation, each future has a unique value — although you probably cannot yet know what that value is. I’ve implemented this notion of futures as part of a library Reactive.

Edits:

  • 2008-04-04: tweaked tag; removed first section heading.

Continue reading ‘Future values’ »

A type for partial values

In simplifying my Eros implementation, I came across a use for a type that represents partial information about values. I came up with a very simple implementation, though perhaps not quite ideal. In this post, I’ll present the interface and invite ideas for implementation. In the next post, I’ll give the implementation I use.

Continue reading ‘A type for partial values’ »