Lambda the Ultimate

Yes, but let us not forget that some valid points of view are more equal than others. ;)

Speaking of which, for the record here, my favorite LtU contributor is Frank Atanassow. I wish he would write more frequent epic threads like this. And I am keen to hear more about his nascent Arrow language (specifically, motivating factors, underlying concepts, anticipated potential). Arrow may one day vindicate Frank's perspectives. I just hope Microsoft does not do a rip-off or, worse yet, hire Frank and thereby own his work.

Ehud, consider me prodded about the FAQ.

in another on-line group that i frequent i recently asked what came after "meta" - is it possible to take the transition from argument to meta-argument, somehow abstract the process and apply it again (i was looking for something more than a second level of quoting!)? obviously the question is too vague/stupid to answer directly, but it provoked some useful comments - the most interesting (to my eyes) was the statement from a mathematician (and general smart person) that category theory was the best approximation he could think of for such an approach.

anyway, whether that makes sense or not, what i'd really like is some good recommendations for an introduction to category theory. the dumber the better.

ps this isn't meant to criticise frank at all - i enjoy his posts too and have learnt a lot.

Wow. Is he ever lucky! 8^)

when your ideas have a sound theoretical basis it's easy to kick everyone else into touch because you're on solid ground and they're not. at least, that's my experience as a physicist - when you understand the way (a lot of) the world works, it's easy make sense of a lot of things - and i'm starting to see that category theory does the same for computing.

Category theory does the same for *explaining* computing. I think it has yet to be conclusively tested whether category theory does the same for *practicing* programming.

(Yes, Frank *is* a sharp guy. I am not ready to concede he's right about everything. Yet.)

(sorry frank, to talk about you as though you are not here)

[later edit] - another example might make things clearer. about 15 years ago when i was at university, a few people were starting to talk about bayesian stats (the timing may depend on the area of study - this was astronomy). they weren't necessarily smarter, but they had clearer explanations for a lot of things that had seemed confusing before. at the time it was a somewhat weird/exotic/fringe thing. now it's accepted and largely the official doctrine. i get the same feeling about category theory.

These are not necessarily introductory texts (in fact, they assume some maths and some type theory), but they are good books to get your teeth into:

@Book{LambekScott8IHOCL, author = "J Lambek and PJ Scott", title = "Introduction to Higher-Order Categorical Logic", publisher = "Cambridge University Press", year = "1984" }

@Book{Taylor99Book, author = "P Taylor", title = "Practical Foundations of Mathematics", publisher = "Cambridge University Press", year = "1999" }

Samin

lambek and scott - the review sounds like this is aimed rather high (and out of print)

taylor - sounds better, but too expensive! (i'll see if the uni of chile has a copy though (partner is a prof there)).

discussed recently

I can't vouch for the book they are using, I haven't read it yet. But looking at the introduction and first few chapters, the authors are aiming for something accessible to high school students.

i also found the following book for free:

Categories, Types and Structures... - The ftp site listed on Amazon doesn't have it, but a little googling turns up http://www.di.ens.fr/users/longo/download.html - http://www.amazon.com/exec/obidos/tg/detail/-/0262011255

And I am keen to hear more about his nascent Arrow language

Hm, yeah, me too. *cough* I must get around to that one of these days... I've been developing some of the ideas vis-a-vis type isomorphisms in recent papers, but it's still very much a diamond in the rough.

some good recommendations for an introduction to category theory. the dumber the better.

The Schanuel and Lawvere text mentioned in the categories discussion group thread is indeed pretty, er, dumb. Not much good for programming, though. Asperti and Longo's Categories, Types and Structures is more useful IMO, but I still think most people will struggle with it, as its a bit short on motivation.

Writing such a text is also perpetually on my own to-do list, but I keep putting it off because I would like to use Arrow programs for the examples.

Category theory does the same for *explaining* computing. I think it has yet to be conclusively tested whether category theory does the same for *practicing* programming.

My position is that if you can explain it (analyze it), you can practice it better.

OTOH, I agree that learning CT will not magically turn you into a better programmer. It may well be the case that the (supposed) correlation between understanding CT and being a good programmer has as much to do with the fact that both require a modicum of intellectual ability as it has to do with increased ability to analyze programs.

I am not ready to concede he's right about everything. Yet.

You'll come around eventually, Patrick. You're too smart not to. ;)

But it's comforting for us category-theory-resisting philistines that his position it not completely unassailable.

Another thing we can learn from the past is the failure of characterizations like "Computing Science is really nothing but X", where for "X" you may substitute your favourite discipline, such as numerical analysis, electrical engineering, automata theory, queuing theory, lambda calculus, discrete mathematics or proof theory. I mention this because of the current trend to equate computing science with constructive type theory or with category theory.

(Not to suggest Dijkstra would approve of the way I do things :-)

It does a good job of "concretizing" some of the intuitions about arrows that some of the other texts take for granted.

It also doesn't rely on an extensive background in group theory, topology, etc. that most of the other common texts do.

Category Theory is not the reason I appreciate Frank's input. It doesn't take CT to dispel the misconceptions that float around in typical language discussions. THAT is why I enjoy reading Frank. He has a way of clearing the smoke from the air.

That said, I wish Frank the best of luck with CT approaches. One never knows what obscure corner of mathematics will bring the next killer app. To cite two examples, fractals and quaternions sat around unused for decades until they were "rediscovered" by CGI animators (1990s) and aerospace flight engineers (1960s), respectively.

just skimming through the first 20 or so pages on the bus last night it becamse a lot clearer how categories, pre-categories and functors fit together to make this useful. and there's a fairly long worked example that, it's pointed out at the end, is hugely general, which i think is pretty neat.

at the moment i can't think of an example of a category where the morphisms are numbers and the composition addition. any suggestions?

(a pre-category is easy - addition on whatever set of numbers you're talking about, but to turn this into a category the morphisms must be number tuples (initial value and increment) to meet the unique-type condition. or am i already confused?)

You just gave it, essentially. All that's left to define is what the objects, identities and typings are. For the objects, you can stipulate only one, arbitrary object, say *; for the identities it has to be the number zero; for the typings, take every number n as n : * --> *.

Of course, this is just a monoid, but every monoid is a category.

(and thanks - i'll shut up after this, because it's not really language related).

[ps - on edit - for example, the category with the single object "1" and the morhpisms that raise it to the nth power would be a solution that seems more in line with the morphisms being numbers]

Since there's so much language research using category theory these days, it's quite on topic for LtU.

I guess so, since I don't know exactly what you mean by the first. :/ Unless you're saying (which I doubt) that the collection of morphisms is denumerable, that is, has size the smallest degree of infinity.

because it seems to me that associating evey number with "* --> *" is stretching what it means for "morphisms are numbers".

Why? Are you sure you understood what I wrote? (Or maybe I misunderstood you.) I meant that every morphism has as domain and codomain the single object of the category.

Maybe I should be clearer. Take Ob = {*} and Ar = Hom(*,*) = N (the naturals). Then cod and dom are forced. Then take id_* as zero, and composition as addition. The result is a category. If you don't believe me, then all you have to do is verify that addition is associative and has zero as a left and right unit (and that typing is preserved, N is a set, blah blah blah).

To say "the morphisms of category C are X" is to say "Ar(C) = X". To say "every morphism has type *-->*" is to say "cod(x)=* and dom(x)=*, for all x in Ar(C)". So I don't see why it's a stretch; I can define cod and dom any way I like, as long as they produce values in Ar(C).

you could replace "number" with "fruit" and nothing would change

Something would change. You can't add fruit. You would need to define a suitable notion of what it means to compose fruits, and what an identity fruit is.

but doesn't the "morphisms are numbers" mean that somehow the morphism has to have a "connection" with numbers - the the value of the number is used by the morphism?

Are you asking if the composition function needs to depend on its arguments?

It doesn't have to, though it usually does. In this case it does, since you need to know what numbers to add.

is this what he's getting at when he talks about categories not dealing with the structure of objects?

Perhaps inasmuch as it doesn't matter what the single object of the category is.

for example, the category with the single object "1" and the morhpisms that raise it to the nth power would be a solution that seems more in line with the morphisms being numbers

To me, "morhpisms that raise it to the nth power" sounds like the morphisms are functions on numbers, not numbers themselves. Are you mixing up morphisms and objects?

(a pre-category is easy - addition on whatever set of numbers you're talking about, but to turn this into a category the morphisms must be number tuples (initial value and increment) to meet the unique-type condition. or am i already confused?)

And now that I've looked at Fokkinga's notes, perhaps I can guess at the source of your confusion. (BTW, he writes tgt/src for my cod/dom.)

You seem to think that the typing relation, which he writes ":", is somehow "universal", or comes as part of Ar. This is why perhaps it seems unnatural to give type *-->* to numbers. But the typing relation is not universal, it is part of the data that define a category. If you prefer, you can write "TYPE-OF(f,a-->b)" instead of "f : a-->b"; and this relation TYPE-OF must be defined for each category. (Actually, it is just a function Ar-->Ob*Ob because of the unique typing requirement.)

Furthermore, TYPE-OF can be (and frequently is) different for categories which nevertheless share the same definitions of Ar, or even both Ar and Ob.

For example, the category Mod(F) of algebras of endofunctor F on some category C has the same arrows as C, but different objects, so TYPE-OF is necessarily different.

The opposite category -C of a category C has the same objects and arrows as C, but TYPE-OF(f,A-->B) in C iff TYPE-OF(f,B-->A) in -C.

A more extreme example is the Kleisli category Kl(T) for a monad T on C. It has the same objects as C, and as arrows all arrows f s.t. TYPE-OF(f,A-->TB) in C; but TYPE-OF is defined like TYPE-OF(f,A-->B) in Kl(C).

(BTW, "precategory" is not a standard concept; Fokkinga only uses it as a means to an end.)

[edit: not sure it's worth explaining what i was doing wrong, but mainly i was confusing "number" with "applying a function, one of whose arguments is a number"]