Loading...

Lambda Jam 2015 - Conal Elliott - Denotational Design: From Meanings To Programs #YOWLambdaJam

10,524 views

Loading...

Loading...

Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Oct 17, 2015

In this talk, I’ll share a methodology that I have applied many times over the last 20+ years when designing high-level libraries for functional programming. Functional libraries are usually organized around small collections of domain-specific data types together with operations for forming and combining values of those types. When done well, the result has the elegance and precision of algebra on numbers while capturing much larger and more interesting ideas.

A library has two aspects with which all programmers are familiar: the programming interface (API) and its implementation. We want the implementation to be efficient and correct, since it’s (usually) not enough to select arbitrary code for the implementation. To get clear about what constitutes correctness, and avoid fooling ourselves with vague, hand-waving statements, we’ll want a precise specification, independent of any implementation. Fortunately, there is an elegant means of specification available to functional programmers: give a (preferably simple) mathematical meaning (model) for the types provided by a library, and then define each operation as if it worked on meanings rather than on representations. This practice, which goes by the fancy name of “denotational semantics” (invented to explain programming languages rigorously), is very like functional programming itself, and so can be easily assimilated by functional programmers.

Rather than using semantics to explain an existing library (or language), we can instead use it to design one. It is often much easier and more enlightening to define a denotation than an implementation, because it does not have any constraints or distractions of efficiency, or even of executability. As an example, this style gave rise to Functional Reactive Programming (FRP), in which the semantic model of “behaviors” (dynamic values) was simply functions of infinite, continuous time. Similarly, the Pan system applies this same idea to space instead of time, defining the semantics of an “image” to be a function over infinite, continuous 2D space. Such meanings effectively and precisely capture the essence of a library’s intent without the distraction of operational details. By doing so, these meanings offer library users a simpler but precise understanding of a library, while giving library developers an unambiguous definition of exactly what specification they must implement, while leaving a great deal of room for creativity about how. I call this methodology “Denotational Design”, because it is design focused on meaning (denotation).

The workshop will present the principles and practice of Denotational Design through examples. I will use Haskell, where purity and type classes are especially useful to guide the process. Once understood, the techniques are transferable to other functional languages as well. If you’d like a sneak peak, see the paper Denotational design with type class morphisms and some related blog articles.

Conal Elliott has been working (and playing) in functional programming for more than 30 years. He especially enjoys applying semantic elegance and rigor to library design and optimized implementation. He invented the paradigm now known as “functional reactive programming” in the early 1990s, and then pioneered compilation techniques for high-performance, high-level embedded domain-specific languages, with applications including 2D and 3D computer graphics. The latter work included the first compilation of Haskell programs to GPU code, while maintaining precise and simple semantics and powerful composability, as well a high degree of optimization. Conal earned a BA in math with honors from the College of Creative Studies at UC Santa Barbara in 1982 and a PhD in Computer Science from Carnegie Mellon University in 1990. His latest position was at Tabula Inc, where he worked on chip specification and compiling Haskell to hardware for massively parallel execution until their closure in early 2015. Before Tabula, his positions included Architect at Sun Microsystems and Researcher in the Microsoft Research graphics group. He has also coached couples and led conscious relationship workshops together with his partner Holly Croydon, with whom he now lives on 20 acres in the woods in the California Gold Country.

For more on Lambda Jam, visit http://www.lambdajam.com

Loading...

When autoplay is enabled, a suggested video will automatically play next.

Up next


to add this to Watch Later

Add to

Loading playlists...