Lambda the Ultimate

The whole paper is predicated on already have a candidate denotational semantics and thus doesn't address why you would want one as opposed to, what you are suggesting, an algebraic semantics. Reasons for using a denotational semantics as opposed to an algebraic one (or an operational one, or axiomatic, etc.) are outside the scope of the paper.

What the paper suggests is a "hygiene" condition for a given denotational semantics. This hygiene condition, though, connects denotational semantics and algebraic semantics.

An algebraic semantics for something characterizes that thing as the initial algebra, i.e. we start with the syntax which is (usually) a free algebra, i.e. an initial algebra for a theory with no equations, and we add equations until we arrive at the mathematical object we want. Here's an algebraic semantics for a language of adding Peano naturals having expressions like: add(s(s(z)), s(s(z)))

Peano : Sort
s : Peano -> Peano
z : Peano
+ : Peano x Peano -> Peano
add(z, n) = n
add(s(n), m) = add(n, s(m))


For a denotational semantics, we also start with the free algebra of syntax, but we simply provide a model for it in terms of some mathematical object we already understand (described however, perhaps algebraically). Here, "model" means an algebraic homomorphism from the syntax (this is the "compositionality" requirement of denotational semantics). Here's a denotational semantics of the same language as above:

[[ ]] : PeanoExpr -> Natural
[[z]] = 0
[[s(n)]] = 1 + [[n]]
[[add(m,n)]] = [[m]] + [[n]]


Given an algebraic semantics, we can define a representation function which is usually used to provide an implementation that is more efficient than the initial algebra. A representation function is an algebraic homomorphism from the initial algebra describing the semantics. So, instead of using effectively data Peano = Z | S Peano would could represent it as natural numbers, but we already have such a representation! The denotational semantics above, since it validates the equations of the Peano algebraic semantics, is a representation of that semantics. A denotational semantics is always a representation of the syntax free algebra. From here, we can view Conal's type class morphisms as adding the operations and laws of a type class to the syntax and then requiring the "meaning function" to be a representation function for the resulting algebraic semantics.

I got a different sense from the abstract and introduction, which is that the denotational semantics were meant to repair some deficiency with a purely algebraic/axiomatic semantics. But even assuming the context you provide, I'm still missing something about the paper. It seems like it would be easier to just say that the semantic function mu should define an instance of each of the type classes it models (which seems somewhat obvious). All mu seems to be doing is collecting canonical instances for a number of type classes and packaging them up as a single function.

The defining power of algebraic semantics comes from initial algebras. When used as an algebraic specification, we lose most of the defining power of the semantics. The laws of type classes are specifications. For example, besides the intended model (the initial algebra) of Peano above (namely the naturals) here are two other models and their representation functions.

U : Peano -> ()
U(z) = ()
U(s(n)) = ()
U(add(m,n)) = ()

Z : Peano -> Integer
Z(z) = 1
Z(s(n)) = 2 * Z(n)
Z(add(m,n)) = Z(m)*Z(n)


No useful type class will uniquely determine an instance (otherwise it might as well be a module). Even combinations of type classes rarely uniquely determine an instance. Without the rest of an algebraic semantics, it is unlikely you'll be able to pin down the meaning adequately. A denotational semantics avoids this by being more direct, i.e. we pick the specific representation. So for example, if we have a module containing an operation add : Integer x Integer -> Integer, this does not provide a basis for making the suggested monoid instance. If we were, additionally, given a semantics that mapped add to addition, then we would be able to prove that the relevant instance was a monoid. And of course, we'd be able to do similar for various other properties that would follow. This is what Conal means by "[Users] care what the names mean." This isn't a failing of interfaces, they are meant to be loose, but when you are describing a particular type/structure the interfaces alone are inadequate. On the flip side, it would be awkward or impossible to give something like the monoid interface using denotational semantics, it would be too specific.

Responding to the latter part of your reply. It is not obvious that the semantic function should define an instance of each type class. Often times the semantic domain is "bigger" than the syntactic domain (in fact, it has to be at least as big as the syntactic domain modulo all the equations we'd like to hold). For example, in the Map example the semantic domain includes values like λx.Just (x+1) which don't correspond to any finite map. As a noddy example, we can use the complex numbers to model the naturals, but while the naturals are totally ordered in a way that preserves their arithmetic structure, the complex numbers are not. The Memo trie example illustrates a domain that is too large in this sense. Another aspect is the slogan is "The instance's meaning is the meaning's instance." What's the meaning's instance? A semantic domain can be an instance of a type class in multiple ways. Which one is "the" meaning's instance? Conal's solution, which is not spelled out, and the one that is slightly less implicit in my previous reply is instead of specifying semantic domains we should specify semantic algebras, i.e. beyond the "carrier set" we should distinguish some operations (i.e. choose specific instances which happens implicitly in Haskell because a type can only be made an instance of a type class once.) If we do this, then we immediately rule out some overly large semantic domains. Also, the fact that our semantic domain is still likely to be strictly larger than our syntactic domain is where the simplicity and generality benefits come from.

With a sufficiently powerful equations, it's possible to pin down types uniquely up to isomorphism (essentially you just require "this type behaves exactly like this other type which it is supposed to denote"). Your new Peano example is isomorphic to the first, so I don't think it should count as a difference (as you say, the whole point of type classes is to allow up-to-isomorphism differences). You didn't include enough Peano axioms to rule out e.g. a model consisting of a single number 0 which is its own successor, but if you axioms like invertibility of s and induction, then you get something that captures the naturals pretty completely (it could have non-standard models, but not in a way that's visible internally). In doing so you enumerate the properties that are going to be useful for proving things about your entities, so I see this as useful. Similarly for any inductive type.

For your example of the complex numbers modeling the naturals, the instance would need to map the type Nat to a subset of C (consisting of the naturals) or certain properties like induction would fail to hold. Similarly for your example of Maps, the type Map should be modeled as a subset of functions (the ones that actually represent maps), not as the type of all functions. (And as an aside, Conal doesn't seem to want *every* type class to have a denotational semantics - just the ones that are acting as ADTs)

The "sufficiently powerful equation" is the constraint of initiality. That applies to my first and only algebraic semantics for Peano. The others were representation functions of that first semantics (using it as a specification rather than a semantics). They are not necessarily initial and thus not necessarily isomorphic to the initial algebra semantics (and conversely). See chapter 12 of this for an introduction to algebraic semantics: Syntax and Semantics of Programming Languages. I am and have been using "algebra" and "algebraic semantics" in a technical sense.

The examples you mention in your second paragraph were with regards to denotational semantics. There is nothing that requires that everything representable in the semantic domain be denotable. When this happens it is called full completeness. It has costs and benefits. My implied denotational semantics for the Complex example is as you said, an injection. This is a perfectly valid denotational semantics and you can prove whatever you'd like about the modelled structure with it. My point was that this valid semantics doesn't satisfy a property that could readily be encoded as a "type class morphism," because the target domain is too big.

Ultimately, you seem to have a misunderstanding of type classes. Several phrases you've made throughout your posts in regards to type classes are nonsensical. You seem to be confusing type classes with something like a module (or even an OO class minus most of the OO-y parts of it.) Here are the phrases don't make sense to me from your most recent post:

"as you say, the whole point of type classes is to allow up-to-isomorphism differences"

I never said this because it doesn't make any sense. Type classes are there to capture similarities between different things, not (just) isomorphic things. Any useful class has non-isomorphic instances. Nearly every type in Haskell is an instance of Show, or Eq. Many are instances of Monoid including functions and () which are certainly not isomorphic.

"Conal doesn't seem to want *every* type class to have a denotational semantics"

Conal doesn't give a denotational semantics to any type class because there's nothing to give a denotational semantics to. A type class is not a particular "thing". A type class is just a bunch of names. When you make an instance of a type class for a particular type, you bind those names to particular values when used at that type. Conal is giving a semantics to particular instances of particular type classes. Type classes are just a mechanism for reusing names.

"just the ones that are acting as ADTs"

Again, type classes aren't things and in particular are not types and so they aren't ADTs. If you meant something like "interfaces to ADTs" even that doesn't work out. Most type classes don't correspond to the interface for an ADT and are not used that way, and type classes aren't very well suited to it. Certainly none of the examples Conal used make sense as ADT interfaces. If all you knew about something was that it was a Monoid, then you wouldn't be able to do anything at all with it, similarly for Applicative, Monad, Functor, Zip. Num is a partial exception; with its interface alone you'd be able to do whatever you could in some subring of the integers, but Integer (and subrings of it) are certainly not the only instances of Num. None of these type classes are a complete interface for a type.

Here is an introduction to type classes in Haskell.

If you like, I can re-present the "type classless" interpretation of Conal's work that I outlined in my previous posts in a more coherent way.

Apologies for being somewhat loose with terminology. [In particular, as you note, I missed the role of initiality in your algebraic semantics.] His paper is about type classes in Haskell, and yet Haskell is not expressive enough to model the various laws that he wants to talk about, so we're either talking about some dependently typed extension to Haskell or we're keeping track of the laws in meta-land.

"Type classes are there to capture similarities between different things, not (just) isomorphic things."

My point was that type classes are intended to capture a mathematical structure, and isomorphic objects have the same structure.

"Conal doesn't give a denotational semantics to any type class because there's nothing to give a denotational semantics to."

This is probably where I misunderstood the paper. I thought he was packaging up the "abstract types" into a type class of their interfaces. Regardless of whether this was intended, it's IMO the simplest way to look at the situation. An abstract type is a set of operations that satisfy some laws, just like a type class. If an abstract type is to be an instance of some type class, then the laws of the type class induce laws on the abstract type. From this viewpoint, a condition for good hygiene on 'mu' is simply that the mapping models the theory of the abstract type (i.e. is an instance of the type class of its interface and satisfies all the laws). I suspect this is equivalent to the TCM condition.

AFAICT, modeling the naturals as a subset of the complex numbers should be a perfectly fine TCM - but the instance is for a subtype, not all of Complex.

His paper is about type classes in Haskell

Not really. He uses them as a presentation tool that his audience is likely to be familiar with as opposed to universal algebra or category theory. Also it is historically how he arrived at the idea. He could just as well have used ML modules (or even Haskell modules) or algebras or some ad-hoc scheme to present the ideas.

so we're either talking about some dependently typed extension to Haskell or we're keeping track of the laws in meta-land

In this particular case the latter is done as the whole paper is about "pencil and paper" reasoning, but the former isn't the only alternative or even the simplest (perhaps it is for Haskell though). Check out the OBJ family of languages for languages that are explicitly based on algebraic semantics and explicitly have theories as objects of the language and yet are not dependently typed.

My point was that type classes are intended to capture a mathematical structure, and isomorphic objects have the same structure.

Yes, but Conal rarely talks about isomorphic objects in this paper (either at the Haskell level or at the "algebra" level.) [To be clear, things isomorphic at the Haskell level need not be isomorphic at the "algebra" level. First, Last, and Maybe are all (trivially) isomorphic as Haskell types, but their Monoid instances do not lead to isomorphic monoids.]

AFAICT, modeling the naturals as a subset of the complex numbers should be a perfectly fine TCM - but the instance is for a subtype, not all of Complex.

Using a subset of Complex would be using a different target semantic domain. My point in using that example was that it is not wrong as a denotational semantics even though the "TCM condition" fails. The "TCM condition", though, can operate as a hygiene condition detecting excessively large semantic domains. That said, it is only a guideline, perhaps I want to use meromorphic functions to study computable sequences in which case N -> C may be exactly what I want.

Hi Matt (M),

Thanks for the remarks.

[...] without answering "Do I want a denotational semantics for my type classes?" What does this extra level of indirection get us over just reasoning algebraically about type classes in the theory they define?

Based on this remark and your other comments, I surmise that we have different biases. For me, denotational semantics is "direct" (satisfies my primary curiosity) and algebraic reasoning is secondary (and justified by the semantics), while for you the reverse.

An ensuing discussion on Phil's post clarified that he'd interpreted my draft as saying that the class laws come "for free" (Phil's words), where I really meant that (a) the laws are guaranteed to hold, and (b) often the proofs have already been "paid for".