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
n is a type-encoded unary number, built up from zero and successor (
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
Applicative. Completing the
Applicative instance is tricky, however. Unlike
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’ »
There has been a scurry of reaction on twitter and reddit to Robert Fischer’s post saying that Scala is Not a Functional Programming Language.
James Iry responded by saying that analogous reasoning leads to the conclusion that Erlang is Not Functional
My first inclination was to suggest that Haskell, as commonly practiced (with monadic IO), is not a functional language either.
Instead, I’m going to explain how it is that the C language is purely functional.
Continue reading ‘The C language is purely functional’ »
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.
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
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!
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
(< *>) in the
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’ »
I submitted a paper Simply efficient functional reactivity to ICFP 2008.
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”).
For quite a while, I’ve been using a handy operation for filtering functional events:
justE :: Event (Maybe a) -> Event a
The idea of
justE is to drop the
Nothing-valued occurrences and strip off the
Just constructors from the remaining occurrences. Recently I finally noticed the similarity with a standard function (in
catMaybes :: [Maybe a] -> [a]
Continue reading ‘A handy generalized filter’ »
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
Continue reading ‘Future values via multi-threading’ »
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.
- 2008-04-04: tweaked tag; removed first section heading.
Continue reading ‘Future values’ »