Lambda the Ultimate

You're talking about polymorphism - when the type operated on does not affect the meaning of the function.

There is also overloading (which is done in Haskell via constrained polymorphism), where, say, every type that has an Eq contract can be compared for equality.

Finally, there is generic or polytypic programming, where a function's behavior depends on the type's shape. To understand this, I think one needs to understand algebraic data types, so you might as well just hop right into Haskell.

You're right that the C++ community uses generic programming in the sense of the STL: parametrically polymorphic collection types, and programming to interfaces. That's why we coined a new term datatype-generic programming for the subject of the project of which the SSDGP school is the terminus. DGP is about programs parametrized by datatypes (such as "list of") rather than by element types. Generic size, which works for any collection type as well as any element type, is an example. One can also write datatype-generic programs for pretty printing, data compression, marshalling, and so on. I tried to explain this in my DPCOOL paper Patterns in Datatype-Generic Programming, and I'll have another go at the School!

Notice that C++ teamplate are related to Ada's generic units (which came first). This is relevant to the terminology discussion, since the word "generic" is part of the Ada syntax for creating parameterized modules ("generic packages" in Ada-speak).

You got close in your first post. Parametric polymorphism allows you to state that a function does not depend on some aspect of the data, e.g. it does not depend on the elements in the list. In the OO world, "generic" often (but not always) means essentially this (though possibly bounded parametric polymorphism that subtyping makes possible). In the statically typed FP community "generic", currently, means polytypic. This means it depends only on the structure of the data and is independent of the content or to an extent the "meaning" of it. A common example is equality. (==) is definitely not a parametrically polymorphic function, it definitely needs to know about what it's testing for equality, but there is a notion of structural equality: a tree is equal to another tree if the values in it's nodes are equal and the children are equal. Most algebraic data types, for example, are trees and the above algorithm will determine a useful and usually "the" equality between them. Polytypic programming lets us essentially implement the above algorithm description giving us one single structural equality function that can be used for any algebraic data type.

(==) is definitely not a parametrically polymorphic function, it definitely needs to know about what it's testing for equality, but there is a notion of structural equality: a tree is equal to another tree if the values in it's nodes are equal and the children are equal. Most algebraic data types, for example, are trees and the above algorithm will determine a useful and usually "the" equality between them.

Is there any difference between this and defining an equality function over s-expressions (e.g. something like Scheme's (equal?) predicate)? Indeed, is there any real difference between algebraic data types and s-expressions? :-)

Algebraic datatypes are typeful in a way that s-expressions aren't, and have more fundamental structure (s-expressions desugar to a pile of cons cells).

Algebraic datatypes are typeful in a way that s-expressions aren't [...]

Well yes, that's the obvious answer, hence the :-) in my post.

[...] and have more fundamental structure (s-expressions desugar to a pile of cons cells).

More fundamental than cons cells? Or do you mean more explicit? Anyway, what I was trying to say was: is polytypic programming "just" a typeful way of doing what (equals?) does in Scheme or is it more than that? There seems to be the idea that you can define some function over all algebraic data-types (ADTs) rather than individually for each type, which goes beyond overloading offered by type-classes (which is per-type overloading). This is presumably possible because all ADTs offer the same basic underlying structure (a tree of constructor field field... values). But whereas in Scheme you can drop-down to defining functions over all ADTs by just treating them as s-expressions, in Haskell the type system enforces a separation and conceals any underlying structural similarity between ADTs of different type. So, further questions:

• Is polytypic/generic programming more than just this ability to "drop down" to a common structure shared by all types?
• Does being able to drop down in this way imply another type-layer (meta-types)? For instance, in an OO language I'd probably do this by making all ADTs be instances of a AlgebraicDataType meta-class.
• If yes to the above, how would/does this type layer interact with (say) Haskell's "kind" system (something I know very little about)?

I meant that the fundamental structure behind ADTs (sum-of-products) has more structure than the fundamental structure behind s-expressions (cons cells).

Polytypic programming mostly seems to be about the ability to analyse the structure of types, yeah - I think generic programming is mostly the interaction between that and (constrained) parametric polymorphism. This does get you more than (equals?) and the like does though, you can't meaningfully define a generic fold or map in the lisps for example because you don't see enough structure to do so (you can, of course, define a fold for binary trees/cons cells and work with that).

Being able to drop down may well imply a kinding system or an AlgebraicDataType typeclass, I'm not sure which of the two is the more sensible way to do it - I suspect it rather depends on the type system in question.

Haskell's kinds are very much "types of types" (where type includes type constructors). It largely makes sure that type constructors are fully applied and things like that. In System Fomega the kind system is in fact the type system of the simply typed lambda calculus!

Btw, if you fancy racking my brain for more info over a pint or something sometime I'd be up for that (and can drag along some reference material if that'd be helpful) - I'm still around notts.

(Fair warning and full disclosure: this (verbose!) explanation is founded on a non-standard approach to the problem which actually pre-dates the term "polytypism", so you must take it with a grain of salt. But I think the pedagogy is still good.)

Consider first how we define functions over values, at least in a functional language with algebraic datatypes. One way is to define the function using a variable parameter, so that we imply nothing about the structure of the potential arguments (assume for now that we do nothing to analyze the structure of the argument within the body of the function definition, either):

f x = ... x ... x ... -- no analysis of x

data T = A | B
f A = ...
f B = ...

In the first case we are treating the argument to the function parametrically, schematically, "with kid gloves"; in the second case we are more violent or invasive, tearing it apart and inspecting its innards, i.e., we are treating it analytically.

The former case is easily re-expressible as a lambda abstraction, whereas the second would require, in general, something more like a pattern abstraction; rather than a single variable and body, we would have multiple pattern/body pairs, and an additional sense of sum-elimination (from a type-theoretic perspective):

λx . e[x]   ::   σ → τ

p₁ ⇒ e₁ | ... | p_n ⇒ e_n   ::   σ → τ

λx . e[x]   ⇔   (x ⇒ e[x]) -- only one "summand"

Λα . e[α]   ::   ∀α. τ[α]

ρ₁ ⇒ e₁ | ... | ρ_n ⇒ e_n   ::   ∀α. τ[α]

This analytical polymorphism (as I called it in my dissertation) has some drawbacks: it allows one to define "ad-hoc" polymorphic functions whose results depend on the structure of the type. In some sense they all do, of course, but in certain cases (such as the map function) we feel that they are spiritually OK, even if they arise from profane beginnings. (In my system, map had a type like this:

map ::   ∀φ. ∀&alpha,β. φ α → φ &beta

In practice there are also many details to be worked out: for example, in a Hindley-Milner system we don't explicitly abstract type arguments with a type abstraction form. Can we actually infer types for definitions and uses of analytically polymorphic functions? (I exhibited a limited form with some annotation required which I called structural polymorphism.) And we must ask ourselves, what is the overall structure of the space of type arguments we are going to analyze with type patterns? Probably atomic types and products will be there, but not function types (well, perhaps you can get one side of the arrow, if not the other). Finally, a successful treatment of user-defined algebraic datatypes requires abstracting over these in some general way, so that we are not stuck working inside a fixed context of algebraic datatpes. (I used variables ranging over constructors, in my dissertation, both type constructors like List and value constructors like nil and cons, but it was naive and messy, and more sophisticated approaches have been developed since then.)

Anyway, I hope this helps with polymorphism versus polytypism. But you should read the works of Johan Jeuring, Ralf Hinze, Patrick Jansson, etc. for the modern story and the real details (I worked on this in the mid to late 80s, dissertation in 92; Tim Sheard also worked on an approach to this in the mid 80s). With the modern versions you can get a real implementation to play with (Generic Haskell) and even more fun toys (such as analytically-defined functions from types to types, etc.).

Thanks for the tutorial, now I have to spend some time understanding it :) I'll also check out Jeuring, Hinze and Jansson.

When you write a function (which therefore will take some argument) there are two basic strategies: you might shuffle the argument around "from the outside", as a black box: pair it with something else, replicate several copies of it, tack it on to the front of a list, etc. Or you might analyze its structure and do something accordingly: rotate it if it's a rectangle, but leave it alone if its a circle; use length and width to calculate its area if its a rectangle, but pi and radius if it's a circle; etc.

In the former "black box" case, you tend to get polymorphic functions, whose types are independent of the argument type, since you might just as well be shuffling anything around: integers, shapes, characters, etc.. It doesn't matter what's in the black box if all you are doing is just moving the box around and never opening it up to look inside.

In the latter case, at least in FP, you use pattern-matching on the argument and proceed by cases: your function will have a specific argument type, such as the shape type used in the examples above, because you will have taken some set number of possibilities into account: circles, rectangles, etc. (and in a functional setting, ignoring classes for the moment, these will be the constructors of some data type: a shape is defined somewhere to be either a circle or a rectangle, etc.).

Now, polymorphic and polytypic values can be thought of as taking a type argument, and doing something with it in order to yield a value result (usually a function). The polymorphic case is like the "black box" case above: you take a type parameter, but you simply use it "from the outside", as a variable in certain places, as an unknown or a placeholder (i.e., parametrically). If you were in an explicitly-typed language, you might use this type parameter by plunking it down in the type constraints that appear somewhere in the body code (say in the type of a function argument).

In fact, you do tend to use such a type parameter as the type of one of the function arguments you're going to shuffle around in the black-box style. For example, given a type, and given an argument of this type, you shuffle around the argument thus ... . The resulting function is something which works for any type precisely because you didn't do anything that depended on it being some specific type.

The polytypic case, on the other hand, is more like the function defined on a specific type by pattern matching. But now we are working at the level of types, i.e., this argument we are going to analyze by cases is in fact itself a type. What are the cases? Oh, I suppose it could be an atomic type (integer, boolean, character, etc.); or maybe it is a pair. Or perhaps it is some recursively-defined type (a list, tree, etc.). But what we seek to do is to cover all possible cases, all possible types that this argument might be (not have, but be: the argument itself is a type!)

We do so by exhaustively covering the possibilities with a big case analysis (pattern matching in my approach) on the possible structure of types. So instead of circle and rectangle as possible cases of a shape argument, we will have (e.g.) integer, pair and list as possible cases of a type argument.

What can we possibly define in this way that is useful? Well, the best examples are a bit more complicated, but the idea is that we can write functions which will work for any type and depend on the structure of the type to determine how they will behave, rather than functions which work for any type because we wrote them to be independent of the types of their arguments. In other words, they work "for all" types because they exhaustively cover all types, not because they studiously avoid doing anything type-specific.

My favorite examples have to do with functions that are polymorphic (oops, polytypic!) in a data structure: size, depth, map, etc., defined not just for lists or for binary trees, or for multi-branch trees, etc., but for any (algebraic) data structure, once and for all. So one gets a single definition of map (structural traversal, essentially) which works for any structure: not by defining a new variant every time one defines a new structure, but rather defining it once, in advance, for all structures, by accounting for all the possibilities in advance. (Again, the details get more complicated, but this is the basic idea.)

Johan, Ralf, Patrick and company do more creative things than just these structural examples: pickling and compression, for example. But again, they write one function which works for all types in advance, so that newly-defined types don't require new code.

So, in summary:

polymorphic = all types by virtue of type-independence
polytypic = all types by virtue of exhaustive analysis of the possible types

That was very clear (at least to me), and the first time I feel like I've really understood the distinction. Nice work!

In the latter case, at least in FP, you use pattern-matching on the argument and proceed by cases

BTW, what about passing the argument to another function, which does perform case analysis? This will break polymorphism of the calling function, right? Ah, the type system will help to detect this efficiently...

One thing that seems related to polytypic programming is (from the FLINT project), Fully Reflexive Intensional Type Analysis that has a type-level typecase (for typing a term-level one).

On a side note, for a good example of how type theorists differentiate between "types" and "tags" (i.e. dynamic "types") Fully Reflexive Intensional Type Analysis in Type Erasure Semantics.