Talk about synchronicity. James Iry wrote about implementing an option type in both Java and Scala. He went on with the expected progression, first explaining what monads are (and a nice explanation that is), following last week with the relation between monadic bind and Scala iterators.
I expect to write a bit more on the list monad, and general tomfoolery with Java generics.
See also Part I.
Update 2007-10-05: I've reworked the code to make it simpler. The insight I had is that, since Java is rank-1 polymorphic, there is no way I can meaningfully abstract over the particular monad being used; however, the monadic class itself is the monadic type constructor. Hence, the type parameters are somewhat simpler.
There are many definitions of monads on the web, many very formal but that don't provide much insight if you're not formally inclined; some very poetic and even somewhat evocative but not very accurate, morally speaking. For our purposes, a monad takes values of type A and "wraps" them in, or marks them as values of type Monad<A>. This wrapper is mostly opaque and inviolable, except for a number of operations that makes using monads less than hopeless:
unit(x) wraps it and turns it into a monadic value of type Monad<A>Monad<B>, bind(f, x) "pipes" a value x of type Monad<A> into f, and returns the corresponding value of type Monad<B>. In effect, bind "lifts" f from taking plain values to accepting monadic values, keeping everything wrapped in the same paper, so to speak.The intent of this rather puzzling machinery is one of representing "special" operations on values by way of their encapsulation in "tainted" procedures that cannot be escaped. The specialness of these operations might reside on their interacting with the environment, or on having "extra" structure on which they depend (state, privilege certificates, etcetera).
These operations must satisfy a number of properties, called the monad laws, with which we won't be concerned here. A monad could have just a little bit of extra structure: if there is a monadic value, call it zero, that satisfies bind(f, zero) = zero for all functions f, the monad is said to be a monad with zero. This is analogous to regular multiplication of numbers. In this case, the monad usually has another operation that "adds" two monadic values into a third, such that adding any value to the zero leaves that value unchanged; this is the monadic addition, and the extended monad is called a monad with plus.
As I wrote in concluding Part I, the Option type gives rise naturally to a monad. This monad is usually conceptualized as the failure monad, which encapsulates computations that might fail to return a value.
Before we start, we need some type-theoretic definitions. We've seen the type-safe functional object:
interface Function<X, Y> {
Y apply(X value);
}
A functor is a parametric type (think of it as a "container type") with an operation map that, given a function f that transforms objects, applies it "inside itself":
interface Functor<X> {
<Y> Functor<Y> map(Function<X, Y> f);
}
Another detail to take into account is that functions are strange with respect to specialization and subtyping. The more specific the return type is, the more specific the function returning it; however, the more specific the function the less specific its argument must be. This is called contravariance, and our functional parameters must take it into account.
To our monads. First, we must define what shape they will have in Java. As a container of values of type X, it can be viewed as a functional. Also, any monad should, at the least, provide a bind (since unit is a kind of "static factory", it cannot be included in the interface signature):
interface Monad<X> extends Functor<X> {
<Y> Monad<Y> bind(Function<? super X, ? extends Monad<Y>> f);
}
The type of bind is complicated by the fact that it must express the covariance-contravariance of its functional argument. A MonadPlus extends a Monad with zero with an operation plus:
interface MonadPlus<X> extends Monad<X> {
MonadPlus<X> add(MonadPlus<X> x);
}
(again, the zero is a static constructor, and cannot be included in the interface.) Now for casting an Option into a Monadic shape (it will actually be a MonadPlus):
abstract class Option<X> implements MonadPlus<X> {
The interface obligations for MonadPlus will be kept implicit; we will use the same trick as before to defer functionality to inner classes. The first case is that of the Some type constructor. It naturally subclasses Option:
public static class Some<X> extends Option<X> {
private final X value;
private Some(X value) { this.value = value; }
The Functor interface requires implementing map. Naturally, it transforms the value and wraps it in a new Some:
public <Y> Option<Y> map(Function<X, Y> f) {
return new Some<Y>(f.apply(this.value));
}
The Monad interface requires implementing bind. For a Some(x) option, it suffices to apply f to its value and return the result:
public <Y> Monad<Y> bind(Function<? super X, ? extends Monad<Y>> f) {
return f.apply(this.value);
}
To comply with MonadPlus interface, the plus operation must return the first argument that is not zero. Since Some is not the zero of the monad, it returns itself:
public MonadPlus<X> add(MonadPlus<X> _) {
return this;
}
}
The other constructor is None:
public static class None<X> extends Option<X> {
private None() { }
The map on it returns None, as tere is no value to supply to f:
public <Y> Option<Y> map(Function<X, Y> _) {
return new None<Y>();
}
Note: I could have returned
thishere, as there is conceptually just one valueNone. However, the type ofthisis parameterized by X while the result must be parameterized by Y. The alternative is to use an unchecked cast,return (None<Y>) this;. This is type-safe but uglier.
Ditto for bind:
public <Y> Monad<Y> bind(Function<? super X, ? extends Monad<Y>> _) {
return new None<Y>();
}
The plus returns its argument, as the left side is this of class None, which by definition is the zero of the monad:
public MonadPlus<X> add(MonadPlus<X> x) {
return x;
}
}
As before, we seal the Option class from extension:
private Option() { }
And let code create optional values using static constructors:
public static <X> Option<X> unit(X x) { return new Some<X>(x); }
public static <X> Option<X> zero( ) { return new None<X>( ); }
}
This completes a type-safe implementation of the Option monad (equivalent to Haskell's MaybeMonad) in Java. We can test its usage:
public class OptionTest {
public static void main(String[] args) {
Function<Integer, Option<Integer>> f = new Function<Integer, Option<Integer>>() {
public Option<Integer> apply(Integer x) {
System.out.println("n = "+x);
return Option.zero();
}
};
Function<Integer, Option<Integer>> g = new Function<Integer, Option<Integer>>() {
public Option<Integer> apply(Integer x) {
System.out.println("n = "+x);
return Option.unit(x + 10);
}
};
final Option<Integer> zero = Option.zero();
zero.add(Option.unit(10)).bind(g).bind(f).bind(g);
}
}
Note that we have to help Java's type checker by assigning Option.zero() to a variable of the right type.
See also Part II.
Andrew Kennedy reminds us that, yes, C# is a functional programming language. So is Java; or at least, Java can encode some of the most advanced idioms that are native to expressive functional languages like Haskell or OCaml. These examples should be straightforwardly translatable to C#.
A algebraic data type or ADT is the type of a choice of values, each of which is a collection, or tuple of other ADT values. In other words, an ADT is a (possibly recursive) "sum of products of types" type. Each option is introduced by a constructor that permits determining to which alternative a value corresponds, and to match it as a pattern to gain access to the constructor's values. Important special cases of ADTs are the list:
type 'a list = Nil | Cons of 'a * 'a list
where Nil —the empty list— is usually called [] and Cons (h, t) —the list with head h and tail t— is denoted by h :: t; and the sum type:
type ('a,'b) sum = Left of 'a | Right of 'b
A special type of sum is the one parameterized on the left by unit, the one-point (uni-valued) type. This special case is called the option type:
type 'a option = None | Some of 'a
This is a good representation for values that "might not be there". Options are used against a destructor, in this case maybe: a higher-order function that discriminates and either applies a function to Some x, or returns a default value for None:
let maybe f e v = match v with | Some x -> f x | None -> e
There is an object-oriented encoding of ADTs that is especially suited for Java: the type is an abstract class declaring visitor methods, and each (algebraic, not object-oriented) constructor or variant is an inner class extending the outer abstract base. With some care with the protection level for the class constructors, this can be tightly sealed so that no extra cases can be added in an external program. I'll illustrate with an encoding for 'a option.
First, a preliminary definition. Java (unlike C#) doesn't have a notion of first-class functions, that is, methods cannot be passed around as they are. The only constructible values are objects; hence we must "simulate" first-class functions with functional classes:
interface Function<X, Y> {
Y apply(X x);
}
We begin by declaring an Option class, parameterized by the type X of the value it encapsulates:
abstract class Option<X> {
The functionality that this class declares, and that its subclasses must implement, is the maybe destructor:
public abstract <Y> Y maybe(Function<X, Y> f, Y e);
The type of the argument is fixed by the class parameter, but the type of the result depends on the particular Function f being used. To enforce encapsulation, this class will not be open to subclassing:
private Option() { }
Now each of Option's subclasses will encode a different variant. First, the inner class corresponding to Some:
static final class Some<X> extends Option<X> {
public final X value;
private Some(X value) {
this.value = value;
}
Only the enclosing class will be able to construct objects of this type. The destructor for a Some object applies the function to the value it represents, and returns the result:
public <Y> Y maybe(Function<X, Y> f, Y e) { return f.apply(this.value); }
}
Now the class corresponding to the None variant. Again, it will be closed to external instantiation:
static final class None<X> extends Option<X> {
private None() { }
Destructing a None value entails simply returning the default value:
public <Y> Y maybe(Function<X, Y> f, Y e) { return e; }
}
Again, only the abstract Option class will be able to construct instances of its subclasses:
public static <X> Option<X> some(X x) { return new Some<X>(x); }
public static <X> Option<X> none() { return new None<X>( ); }
}
This is not as general as a parametric visitor over the composite type, but is much simpler. With sufficiently rich functional objects, both approaches are interexpressible. We can test that everything works:
public class OptionTest {
public static void main(String[] args) {
Function<Integer, String> string_of_int = new Function<Integer, String>() {
public String apply(Integer value) { return value.toString(); }
};
Option<Integer> p = Option.some(10);
Option<Integer> q = Option.none();
System.out.println("p = " + p.maybe(string_of_int, "no value"));
System.out.println("q = " + q.maybe(string_of_int, "no value"));
}
}
We'll see next how Option naturally gives rise to a monad, and how to implement a monad in Java.
EWD797, "Fibonacci numbers and Leonardo numbers" begins with a disclaimer: The following formal derivations and computations are absolutely elementary and without scientific interest.
It uses, however, a simple method to resolve the generating function (used again in EWD801) which is less general than the one explained in Concrete Mathematics or in generatingfunctionology (highly recommended, by the way) but very easy to use.
It then goes on to mention Leonardo numbers:
L.0 = L.1 = 1 L.n = L.(n-1) + L.(n-2) + 1
and explaining that, since the recurrence is not homogeneous, said method cannot be applied.
It then proceeds to pull off a rabbit out of the hat, by rewriting:
(0) (L.n + 1) = (L.(n-1) + 1) + (L.(n-2) + 1)
This trick is quite nifty and not too subtle; what follows, however, is rather flashy: and we immediately derive:
L.n = 2·F.n - 1
Maybe I'm dense and the immediacy of the derivation is staring me in the face; I cannot justify the identity, other than by saying that yes, by induction it is true. So here is what I think.
First, I can tell that (0) is implied by
(1) L.n = F.n - 1
This, however, fails for L.0 and L.1. What is then the simplest adjustment I can perform on (1) that satisfies the base? Well, since F.n = F.(n - 1) + F.(n - 2), I can multiply through a constant, call it k:
k·F.n = k·F.(n - 1) + k·F.(n - 2)
and equate with (0) to get L.n = k·F.n - 1. By solving the base case, we have that L.0 = k·F.0 - 1 forces k = 2.
This I don't find immediate.
I find Edsger W. Dijkstra's talk "How Computing Science created a new mathematical style", recorded in the manuscript EWD1073 one of his most beautiful. Not only is it a clear exposition of his calculational approach to mathematics, to me it is especially poignant since it carries with it the weight of thirty years of experience with the discipline. As such is not so much a promotional piece as a survey of results.
Many things in this talk struck me as worthy of reflection; one thing that stood out was the two examples he gave of how computer science informed (or ought to inform) mathematical discipline:
In order to prove that a compiler correctly parses the program texts it processes, one needs a formal grammar for the syntax of the programming language in question. To formal language theory we owe the distinction between grammars that are "context-free" and those that are not. Next we observe that the manipulating mathematician does not manipulate just strings of symbols but manipulates formulae parsed according to the underlying grammar. Since the parsing problem is simpler for context-free grammars, the moral is simple: choose for one's formalisms context-free grammars.
The other example is the notion of abstract data types —stacks, trees, permutations, bags, configurations, what have you—. Identifying an appropriate data type and some operations on it is often essential in preventing a program from becoming totally unwieldy. In exactly the same way calculational proofs of the desired brevity and clarity can often be obtained by the use of a specifically designed, special-purpose calculus. I said "exactly the same way" because I see no difference between the virtues of a data type in a program and the virtues of a calculus in a proof.
Much is written nowadays about how DSLs enhance the quality of code in complex systems; here is a forceful argument about DSLs enhancing mathematical reasoning.
As an example of this, and because I felt absolutely in awe at the simplicity and transparence of the proof and I think it deserves to be repeated, here is Dijkstra's proof of the Induction Principle:
Theorem: (C, <) is well-founded if and only if mathematical induction over C with respect to < is a valid proof technique.
(C, <) is well-founded
≡ { definition of well-foundedness }
(∀ S :: (∃ x :: x ∈ S) ⇒ (∃ x :: x ∈ S ∧ (∀ y : y < x : y ∉ S)))
≡ { contrapositive and Laws of de Morgan }
(∀ S :: (∀ x :: x ∉ S) ⇐ (∀ x :: x ∉ S ∨ (∃ y : y < x : y ∈ S)))
≡ { transforming the dummy: S = { x | ¬P.x }, P.x ≡ x ∉ S }
(∀ P :: (∀ x :: P.x) ⇐ (∀ x :: P.x ∨ (∃ y : y < x : ¬ P.y)))
≡ { predicate calculus }
(∀ P :: (∀ x :: (∀ y : y < x : P.y) ⇒ P.x) ⇒ (∀ x :: P.x))
≡ { definition of proof via mathematical induction }
mathematical induction over (C, <) is valid
