Conal Elliott

The post Fixing lists defined a (commonly used) type of vectors, whose lengths are determined statically, by type. In Vec n a, the length is n, and the elements have type a, where n is a type-encoded unary number, built up from zero and successor (Z and S).

infixr 5 :<

data Vec ∷ * → * → * where
  ZVec ∷                Vec Z     a
  (:<) ∷ a → Vec n a → Vec (S n) a

It was fairly easy to define foldr for a Foldable instance, fmap for Functor, and (⊛) for Applicative. Completing the Applicative instance is tricky, however. Unlike foldr, fmap, and (⊛), pure doesn’t have a vector structure to crawl over. It must create just the right structure anyway. I left this challenge as a question to amuse readers. In this post, I give a few solutions, including my current favorite.

You can find the code for this post and the two previous ones in a code repository.

Continue reading ‘Doing more with length-typed vectors’ »

The post Fixing lists defined a (commonly used) type of vectors, whose lengths are determined statically, by type. In Vec n a, the length is n, and the elements have...

In the post Memoizing polymorphic functions via unmemoization, I toyed with the idea of lists as tries. I don’t think [a] is a trie, simply because [a] is a sum type (being either nil or a cons), while tries are built out of the identity, product, and composition functors. In contrast, Stream is a trie, being built solely with the identity and product functors. Moreover, Stream is not just any old trie, it is the trie that corresponds to Peano (unary natural) numbers, i.e., Stream a ≅ N → a, where

data N = Zero | Succ N

data Stream a = Cons a (Stream a)

If we didn’t already know the Stream type, we would derive it systematically from N, using standard isomorphisms.

Stream is a trie (over unary numbers), thanks to it having no choice points, i.e., no sums in its construction. However, streams are infinite-only, which is not always what we want. In contrast, lists can be finite, but are not a trie in any sense I understand. In this post, I look at how to fix lists, so they can be finite and yet be a trie, thanks to having no choice points (sums)?

You can find the code for this post and the previous one in a code repository.

Edits:

• 2011-01-30: Added spoilers warning.
• 2011-01-30: Pointer to code repository.

Continue reading ‘Fixing lists’ »

In the post Memoizing polymorphic functions via unmemoization, I toyed with the idea of lists as tries. I don’t think [a] is a trie, simply because [a] is a sum...

I have another paper draft for submission to ICFP 2009. This one is called Beautiful differentiation, The paper is a culmination of the several posts I’ve written on derivatives and automatic differentiation (AD). I’m happy with how the derivation keeps getting simpler. Now I’ve boiled extremely general higher-order AD down to a Functor and Applicative morphism.

I’d love to get some readings and feedback. I’m a bit over the page the limit, so I’ll have to do some trimming before submitting.

The abstract:

Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has also been tackled, though with extra complexity. This paper develops an implementation of higher-dimensional, higher-order differentiation in the extremely general and elegant setting of calculus on manifolds and derives that implementation from a simple and precise specification.

In order to motivate and discover the implementation, the paper poses the question “What does AD mean, independently of implementation?” An answer arises in the form of naturality of sampling a function and its derivative. Automatic differentiation flows out of this naturality condition, together with the chain rule. Graduating from first-order to higher-order AD corresponds to sampling all derivatives instead of just one. Next, the notion of a derivative is generalized via the notions of vector space and linear maps. The specification of AD adapts to this elegant and very general setting, which even simplifies the development.

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!

I have another paper draft for submission to ICFP 2009. This one is called Beautiful differentiation, The paper is a culmination of the several posts I’ve written on derivatives and...

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!

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...

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

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’ »

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...

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.

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’ »

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...

While working on Eros, I encountered a function programming pattern I hadn’t known. I was struck by the simplicity and power of this pattern, and I wondered why I hadn’t run into it before. I call this idea “semantic editor combinators”, because it’s a composable way to create transformations on rich values. I’m writing this post in order to share this simple idea, which is perhaps “almost obvious”, but not quite, due to two interfering habits:

• thinking of function composition as binary instead of unary, and
• seeing the functions first and second as about arrows, and therefore esoteric.

What I enjoy most about these (semantic) editor combinators is that their use is type-directed and so doesn’t require much imagination. When I have the type of a complex value, and I want to edit some piece buried inside, I just read off the path in the containing type, on the way to the buried value.

I started writing this post last year and put it aside. Recent threads on the Reactive mailing list (including a dandy explanation by Peter Verswyvelen) and on David Sankel’s blog reminded me of my unfinished post, so I picked it up again.

Edits:

• 2008-11-29: added type of v6 example. Tweaked inO2 alignment.

Continue reading ‘Semantic editor combinators’ »

While working on Eros, I encountered a function programming pattern I hadn’t known. I was struck by the simplicity and power of this pattern, and I wondered why I hadn’t...

This post is part four of the zip folding series inspired by Max Rabkin’s Beautiful folding post. I meant to write one little post, but one post turned into four. When I sense that something can be made simpler/clearer, I can’t leave it be.

To review:

• Part One related Max’s data representation of left folds to type class morphisms, a pattern that’s been steering me lately toward natural (inevitable) design of libraries.
• Part Two simplified that representation to help get to the essence of zipping, and in doing so lost the expressiveness necessary to define Functorand Applicative instaces.
• Part Three proved the suitability of the zipping definitions in Part Two.

This post shows how to restore the Functor and Applicative (very useful composition tools) to folds but does so in a way that leaves the zipping functionality untouched. This new layer is independent of folding and can be layered onto any zippable type.

You can get the code described below.

Edits:

• 2009-02-15: Simplified WithCont, collapsing two type parameters into one. Added functor comment about cfoldlc'.

Continue reading ‘Enhancing a Zip’ »

This post is part four of the zip folding series inspired by Max Rabkin’s Beautiful folding post. I meant to write one little post, but one post turned into four....

I read Max Rabkin’s recent post Beautiful folding with great excitement. He shows how to make combine multiple folds over the same list into a single pass, which can then drastically reduce memory requirements of a lazy functional program. Max’s trick is giving folds a data representation and a way to combine representations that corresponds to combining the folds.

Peeking out from behind Max’s definitions is a lovely pattern I’ve been noticing more and more over the last couple of years, namely type class morphisms.

Continue reading ‘Another lovely example of type class morphisms’ »

I read Max Rabkin’s recent post Beautiful folding with great excitement. He shows how to make combine multiple folds over the same list into a single pass, which can then...

Lately I’ve been playing again with parametric surfaces in Haskell. Surface rendering requires normals, which can be constructed from partial derivatives, which brings up automatic differentiation (AD). Playing with some refactoring, I’ve stumbled across a terser, lovelier formulation for the derivative rules than I’ve seen before.

Edits:

• 2008-05-08: Added source files: NumInstances.hs and Dif.hs.
• 2008-05-20: Changed some variable names for clarity and consistency. For instance, x@(D x0 x') instead of p@(D x x').
• 2008-05-20: Removed extraneous Fractional constraint in the Floating instance of Dif.

Continue reading ‘Beautiful differentiation’ »

Lately I’ve been playing again with parametric surfaces in Haskell. Surface rendering requires normals, which can be constructed from partial derivatives, which brings up automatic differentiation (AD). Playing with some...