Purely algebraic abstractions

Any abstraction expresses something all its instances share. Usually this is semantic: all instances have some common meaning. They represent the same values, or perform the same computation, or support the same operations. When you know a construct is an instance of a certain abstraction, you know something about what it means.

Some abstractions are different. Their instances have no meaning in common, only algebraic properties. These are purely algebraic abstractions. Such an abstraction tells what transformations are valid on its instances' expressions, but says nothing about what they mean.

The classic algebraic abstractions are (of course) those of abstract algebra: groups and rings and fields and such. They abstract the properties necessary for algebraic transformations, and nothing else. If you know that your objects and their operators form a ring, you can manipulate formulae and even prove theorems about them, without knowing anything about what they mean.

In contrast, most abstractions in computing focus on meaning, and express algebraic properties only incidentally. If you have a java.util.Collection or a java.util.Map, you know you can add and remove items, test whether they're there, and iterate over them — but do you know any algebraic properties? Even the most basic properties are broken by unusual collections like caches or Bloom filters. They're semantically legitimate collections, and their algebraic properties are unreliable because they're irrelevant.

(Algebraic abstractions are not entirely reliable either, because most of their computational incarnations don't quite satisfy their axioms. Reflection and other debugging features can often detect differences between supposedly equivalent objects. Limitations of memory and time create edge cases where expressions equivalent in denotation are different in operation. Floating-point arithmetic makes a sport of breaking nearly every algebraic property that could be expected of it. But similar problems afflict nearly all attempts to reason about abstractions; they're not specific to algebraic abstractions, and they don't make them useless. The equivalences generally hold for the properties we care to preserve, so they're correct in practice though not in theory.)

Haskell typeclasses

Most Haskell typeclasses have semantic content: Show and Num are about operations with the same meaning for all their instances; Eq expects algebraic properties (reflexivity and transitivity) but still defines the meaning of ==. There are a small but increasing number of purely algebraic typeclasses: the Prelude has Monoid, Functor, Applicative and Monad, whose instances have nothing in common but algebraic equivalences.

This is why monads are so hard to learn. Each student of Haskell asks what monads mean, and invents a variety of wrong answers (typically semantic generalizations of IO actions), because they're sure that such an important abstraction must be meaningful, and have never heard of algebraic abstraction. Eventually they learn to use monads without asking what they mean, because monads don't mean anything.

This is a sore point among Haskellers. It will get more sore, because Haskell is gaining more algebraic abstractions. Applicative is in the Prelude now!

Haskell Prime numbers

Haskell Prime is a collection of ideas for future versions of Haskell, including a proposal to generalize the numeric typeclasses by removing their semantic content, replacing Num and most of its subclasses with purely algebraic classes:

(+) :: AbelianGroup a ⇒ a → a → a
(*) :: Ring a ⇒ a → a → a
(/) :: DivisionRing a ⇒ a → a → a
mod :: EuclideanDomain a ⇒ a → a → a

(A division ring is like a field except that multiplication is not necessarily commutative.)

This makes the numeric operations maximally general, at the cost of making them meaningless. It also gives mundane code types (and type errors) that make sense to mathematicians and no one else:

factorial :: (Ring a, Ord a) ⇒ a → a
sum :: AbelianGroup a ⇒ [a] → a

(I'm not sure why + is on AbelianGroup instead of something more general like Magma. Maybe it's to comply with users' expectation that + be associative and commutative.)

This proposal brings the straightforward clarity of Monad to arithmetic, an area where Haskell has long suffered from comprehensibility bordering on practicality.

I'm not sure algebraic abstractions are always a bad idea for programming languages, but the difficulty of Monad suggests they're hazardous.

A semantic abstraction tells you what its instances mean. An algebraic abstraction only tells you what transformations preserve that meaning. That's enough for optimization, but not for understanding.

Oversimplifying bottom

There are a few things that bother me about the usual treatment of ⊥ in Haskell culture:

Multiple failures

I'm uncomfortable with the practice of treating all failures as a single ⊥ value, since they're actually distinguishable. Haskell denotations (ignoring side effects and implementation-dependent behavior) look like this¹:

data Denotation = Return Value | Throw Exception | Nontermination

The traditional ⊥ combines the Throw and Nontermination constructors. Since catch/handle can distinguish different exceptions, these are actually many different denotations, not one.

This must be a standard objection. The obvious response is that the distinctions between bottoms are usually irrelevant, and ignoring them makes reasoning about programs easier, even if it does occasionally give incorrect results. This isn't consistent with usage in the Haskell community, though, because Haskellers use ⊥ most when they want rigor. Nor is it consistent with the rest of Haskell culture, which generally frowns on unsafe shortcuts.

Haskellers appear to be aware of this, but they usually ignore it. I suspect this is due partly to a distaste for denotations outside the Return branch — exceptions aren't “proper” values and don't deserve attention.

This does cause confusion. For instance, it leads ezyang, when discussing definedness monotonicity, to identify nonmonotonic functions as uncomputable, without mentioning that this applies only to nontermination, not to other bottoms. When he later discusses distinguishing between bottoms, he calls this “a very operational notion” and ignores the possibility of catching exceptions — perhaps because Haskell discourages this by putting catch and handle in IO, even though there's nothing impure or unsafe about them.

The bottom type and the bottom value

Haskell culture also traditionally conflates the failure ⊥ with the bottom type, i.e. the values that are members of every type. This is understandable, since they coincide in Haskell — but that's a quirk of Haskell, not a law of denotational semantics.

It happens to be the case in Haskell that failures are the only denotations found in every type. But this is because Haskell types describe only one of the three branches of the denotation. A Haskell type describes what values an expression might return, but says nothing about exceptions or nontermination. If Haskell types could also specify whether an expression might terminate, and what exceptions it might throw (as in Java and C++), then the bottom type would be empty. (And type inference would be undecidable, which is why Haskell doesn't do it.) Failures are in the bottom type only because Haskell's type system can't talk about them.

It's also possible for the bottom type to contain values that aren't failures. For example, if Java didn't have primitive types, its null would be a bottom value, since it's a member of every (static) type. But it's not a failure: there are still useful operations on it, e.g. ==. Nor is it a zero of most operations.

It's probably safe to identify these two bottoms when speaking only of Haskell, but it seems to me Haskellers often do so even when speaking of denotational semantics in general.

Weakness is strength?

I worry that the treatment of ⊥ stems from a pattern of treating Haskell's weaknesses as strengths, or as inevitable mathematical results, rather than as accidents of one language. For example, some Haskellers consider definedness monotonicity a virtue rather than a weakness. (Inability to handle errors makes it easy to prove that your program doesn't recover from them, but hard to make the program do so!) There might be something similar in attitudes to type system extensions, but I don't understand this area well enough to tell.

What do Haskellers (particularly denotationalists) think about this?

Added 6 Sep: Most of these issues (catch is impure, bottom type = bottom value, monotonicity) involve treating quirks of Haskell as universal, but the conflation of multiple bottoms is the reverse: people ignore part of Haskell's semantics in favour of a simpler approximation.

A long footnote about denoting denotations

¹ The usual definition of Haskell denotations is that of Peyton Jones et al. in A semantics for imprecise exceptions: to hide the effect of implementation-dependent evaluation order on exceptions (e.g. what exception does 1/0 + undefined throw?), failure denotations give not a single exception but a set of possible exceptions. In addition, nontermination is treated as an exception, so denotations look like this:

data Denotation = Return Value | Throw [Exception]

Since even return values can be implementation-dependent, I think it's cleaner to make the whole denotation a set of implementation-dependent results. Also, nontermination is quite different from exceptions, in both implementation and semantics: it's a zero of catch, so any attempt to detect it will also give Nontermination. (This is apparently not considered an important distinction in formal semantics, but it's very different operationally.) This gives a slightly more complicated definition:

data Result = Return Value | Throw Exception | Nontermination
type Denotation = [Result]

Actual implementations invariably pick one result, so the complexity of treating a denotation as a set of possible results is usually irrelevant and can be ignored, leaving this definition of a denotation-as-implemented:

data Denotation = Return Value | Throw Exception | Nontermination

If nontermination is treated as an exception, this becomes pleasingly conventional:

type Denotation = Either Exception Value

Haskell and syntactic complexity

Why isn't if a function in Haskell?

In most languages, if is a special form (or local equivalent). That's because if is lazy in its last two arguments, so it can't be a function in an eager language. But Haskell has no trouble with laziness; if can trivially be a function, with no need for special semantics, let alone syntax. There's even a page on the Haskell Wiki advocating switching to the simple functional if.

All this must have been obvious to the designers of Haskell. So why did they choose the Algolesque if ... then ... else ... syntax instead?

Of course this question has come up before. Paul Hudak, one of the designers, explains:

Dan Doel's answer is closest to the truth:

I imagine the answer is that having the syntax for it looks nicer/is clearer. "if a b c" could be more cryptic than "if a then b else c" for some values of a, b and c.

except that there was also the simple desire to conform to convention here (I don't recall fewer parentheses being a reason for the choice). In considering the alternative, I remember the function "cond" being proposed instead of "if", in deference to Scheme and to avoid confusion with people's expectations regarding "if".

To my eye, if a then b else c improves neither clarity nor familiarity, but evidently the Haskell designers thought otherwise. More interestingly, they didn't think the added syntactic complexity was much of a problem. How can this be? Doesn't Haskell culture value simplicity?

Yes, but not so much simplicity of syntax. I'm misled here by a superficial resemblance between the cultures of Haskell and Lisp. Both cultures are obsessed with mechanically processing code, and therefore want the language core to be as simple as possible. Since a minimal core is impractical to program in, both expect a larger, more useful language to be defined by translation to the core, so its complexity can be mechanically eliminated. And both consider the representation of code as text to be separate, at least in principle, from the core. So at first glance, it seems as if they should have the same attitude to syntactic complexity.

But they treat it quite differently. Lisp's culture considers syntax unimportant, and therefore tries to make it as simple and transparent as possible, so it won't prevent humans from seeing through it — because code is much more interesting than its textual representation. But Haskell's culture considers syntax safely separate from the language core, and is therefore willing to tolerate complexity in it. Since it goes away without inflicting any complexity on the core, why shouldn't it include whatever features are convenient?

This approach has given Haskell one of the prettiest syntaxes in the world, so I can't say it's wrong. It is uncomfortable, though, for a Lisper to see a culture which draws wildly different conclusions from seemingly similar premises. Maybe this is explained by modest differences in degree: Haskell values textual beauty a bit more than Lisp, and code-processing a bit less. Is that enough to explain the difference? I don't know. I don't understand.

Mainstream at last!

Functional programming is slowly becoming popular. Yesterday I heard someone refer to Haskell as a "mainstream language". ^_^