Lambda the Ultimate

From your example, I thought that you might have been suggesting just that Haskell support 'deriving Functor' for applicable type definitions.

But what exactly do you mean by types becoming identity functions?

I just read up on GHC's new "deriving Functor" mechanism. Automating the definition of a types fmap is welcome, but is fairly indirect: from a type, it generates an instance of a type class and defines its fmap member, which entails a number of complications relating to module visibility, multiparameter typeclasses, etc.

If Haskell supported reasoning about values at compile-time, as dependent-typed languages like Cayenne do, then a type t could be equated to its identity function

   t_id :: t->t
   t_id x=x

and then the parametric type definition currently written as

   data List t = Nil | Cons t (List t)

could instead be the parametric functor definition

   data List f = Nil | Cons f (List f)

So, instead of defining the list type using Haskell's data syntax, you're defining the list functor using an extended data syntax. This function can be used for reasoning about identity functions, since a functor F applied to an identity function id::t-> yields a new identity function id'::F(t)->F(t). Thus "List Int" in the List-functors-with-types-as-identity-functions world behaves identically to "List Int" in the List-type-with-ordinary-Haskell-types world.

So, instead of defining two things (a parametric type T t, and a function fmap::(t->u)->T(t)->T(u), we would define a single parametric function F f. Given an identity function t, F t would equate to the old T t. And F f replaces the old fmap f.

I'm not suggesting Haskell be redesigned around an approach like this. But, if you're building a dependent-typed language, it's a big win.

When you define the functor (List f), doesn't that still need to create the List data type? Just declaring (List t) to be an identity function on (List t) seems circular. If all the same semantics for data types are still present, what's the advantage of making this identification? So that we can use the name of a type instead of 'id'? Or the name of a functor instead of 'fmap'?

Also, how do co-functors (or more complicated data types) fit into this? data Foo t = Foo t->Int, etc.

The real simplification is that you can write a single lambda-free definition that provides both the type and functor behavior without resorting to typeclass derivation tricks.

Deriving a functor from a parametric type definition requires that the type parameters be used with consistent variance. The previous examples were covariant, but the technique also works with contravariant uses, and scales up to multiparameter functors with mixed variance.

   -- Covariant functor.
   Bar t = Bar Int->t
   map f (Bar g) = Bar (\x -> g (f x))

   -- Contravariant functor.
   Foo t = Foo t->Int
   map f (Foo g) = Foo (\x -> f (g x))

…this approach can work at a more fundamental level in a programming language by extending regular type definitions to functor definitions automatically.

GHC can now derive 'fmap', though the user guide does not explain for what types it can do so. This ticket explains in more detail.

Of course, you can also do this with DrIFT, derive, and generic classes.

You could also derive Functor with Generic Haskell, but it has bit-rotted (and even domain name rotted).

{-# LANGUAGE DeriveFunctor #-}
data Tree t = Leaf t | Node (Tree t) (Tree t) deriving Functor

I can't keep track of which extensions have made it into the ghc distribution, but there may additionally be at least one for full-blown generic programming in there these days.

...this is less interesting than I hoped. :(

IMO, what we really want is the map action for the functor Tree is a fixed point of (what ML and Haskell programmers call "two-level types"). This action is really what lets you avoid writing boilerplate code. For example, suppose you have a little expression language:

  type exp = Var of string | Let of string * exp 
           | Plus of exp * exp | Times of exp * exp | Minus of exp 
           | IfZero of exp * exp * exp 

Now, suppose we write a substitution function replacing variables with numbers. We'll need to explicitly give cases for all the structural cases, which is entirely redundant:

let rec subst n x = function
  | Var y when x = y -> Lit n
  | Let(y, e1, e2) when x = y -> Let(y, subst n x e1, e2)
  (* all this is boilerplate *)
  | Var y              -> Var y
  | Let(y, e1, e2)     -> Let(y, subst n x e1, subst n x e2)
  | Plus(e1, e2)       -> Plus(subst n x e1, subst n x e2)
  | Times(e1, e2)      -> Times(subst n x e1, subst n x e2)
  | Minus e            -> Minus (subst n x e)
  | Lit n              -> Lit n
  | IfZero(e1, e2, e3) -> IfZero(subst n x e1, subst n x e2, subst n x e3)

But if we had the expression type's underlying functor and map action:

type 'a expF = Var of string | Let of string * 'a * 'a
         | Plus of 'a * 'a | Times of 'a * 'a | Minus of 'a | Lit of int
         | IfZero of 'a * 'a * 'a

let map_expF f = function 
  | Var y              -> Var y
  | Let(y, e1, e2)     -> Let(y, f e1, f e2)
  | Plus(e1, e2)       -> Plus(f e1, f e2)
  | Times(e1, e2)      -> Times(f e1, f e2)
  | Minus e            -> Minus (f e)
  | Lit n              -> Lit n
  | IfZero(e1, e2, e3) -> IfZero(f e1, f e2, f e3)

type expr = In of expr expF

Then it's easy to write a succint substitution function which only requires writing code for the cases where something interesting happens.

let rec subst n x (In e) =
  In(match e with 
     | Var y when x = y -> Lit n
     | Let(y, e1, e2) when x = y -> Let(y, subst n x e1, e2)
     | _ -> map_expF (subst n x) e)

You certainly already know that, but it is also interesting to point out that given that "derecursified" type and its `map` operator, you can easily derive fold and unfold :

fold f = f . map (fold f) . unFix
unfold f = Fix . map (unfold f) . f

(Fix/unFix being the boxer/unboxer of your equirecursive types, and are unnecessary with isorecursive types)

Unfortunately, I don't think this paper is perfect, either, but the flaws are probably fixable in revisions. I could also see it being rejected for lack of heavyweight technical machinery. I agree that it bites off a more manageable amount for a single intro paper, but unfortunately one may be left with the feeling that this is merely a cute notation without a lot of new applications. It seems to be a tough tradeoff for a single paper, but we have to start somewhere. I do wonder if it will be accepted... The "folklore" problem only gets worse as the number of species papers circulated in draft increases...

Note that it was submitted as a Pearl, so it is understood that this is an introduction to known work (but with a rather nice Haskell implementation). I am completely convinced there are a lot of applications - see the concluding paragraph of Yorgey's paper for the areas where I (also) believe the main ones lie, which we'd tried to indicate in our earlier draft. Actually, Gordon and I are working on 'testing' (a la QuickCheck and SmallCheck) right now, because of exactly this motivation to show the usefulness of species.

I share your conviction and look forward to seeing the results of your work!

[I can't offhand answer your question about k-permutations]

The basic species are far from ad-hoc: they are called 'atomic species' and correspond exactly to certain group actions (exactly == bijectively). There is a fundamental decomposition theorem for species which says that they call be decomposed into sums of products of atomic species. The basic species that are then used in examples are the ones that "show up" earliest, since species come with a grading.

The combinators are a little bit ad hoc, but easily justified: most of them correspond to very natural operations on formal power series OR very natural operations on combinatorial structures OR very natural categorical operations. The main combinators are those which are in fact 'natural' in all 3 senses.

All of this is carefully explained in the Bergeron-Labelle-Leroux book (end of chapter 2).

The book he refers to is this one: Combinatorial Species and Tree-like Structures. It's an enjoyable read and also a must-read for anyone interested in species.

Thank you for clarification!

There is a fundamental decomposition theorem for species which says that they call be decomposed into sums of products of atomic species. The basic species that are then used in examples are the ones that "show up" earliest, since species come with a grading.

The part that confused me was that the notion of atomic was "not atomic enough" - some of atomic species are not basic (e.g., E product E, IIRC). Thus the decomposition theorem does not explain the choice of basic species. I think I indeed need to read the book... Thanks again!

E product E is not atomic, it is 'molecular'. E is atomic.

Sorry, I should have checked my notes - I meant E2 o E2 (composition).

I'm at a conference in Paris without access to my own notes, and this is not an 'easy' question. I will return to this when I get back.