> Wow, that's a new word, "posetal". Does that mean "can be partially ordered"?

Posetal means that Hom(A,B) has at most one element (the category is "thin"), and that any two isomorphic objects are equal (the category is "skeletal"; corresponds to antisymmetry). So the category can be seen as a poset, where (A <= B) iff Hom(A,B) is nonempty.

> What is "Int"? Integers? Integral? Int... ernal? ... types?

Integers. I was just picking an example type, as lmm says. I could have said: "Fix a type A, and consider f(B) = A -> B".

> What's with the notation, anyway? Why use "<:" instead of "<" like you would for any other transitive anti-symmetric relation?

Tradition. <= is also perfectly fine. Why do set theorists write \subseteq instead of \leq? \subseteq is also a reflexive, transitive, antisymmetric relation.

> "Anti-monotone" is weird language. I would say "monotone" in general and "increasing" or "decreasing" in particular.

Yeah, in analysis "monotonically increasing/decreasing" is more common. I find it more useful to explicitly draw out the fact that one is the reversal of the other; also "monotone" is more concise than "monotonically increasing". shrug

> What does any of this have to do with programming languages? I mean, types are purely abstract, right? Do they have to be part of a programming language? I thought types were merely sets ordered by inclusion.

Well, the OP was about types in programming languages. Types in PLs are not always best thought of as sets; for example, the equation

a = (a -> Bool) -> Bool

has solutions in some type theories! Interpreted in the naive way, this would be a set equal to the powerset of its powerset, which is impossible. This conundrum leads to the study of Scott domains, for example.

> If programming languages are not something that can be abstracted away, what's a programming language in this context? A set (class?) of types and functions on those types?

I'm being deliberately vague on that front. How to define "programming language" is not something widely agreed upon. But similar patterns, such as co- and contra-variance, recur.

> What is a definable function? Are some functions not definable? Is it something like "there exists a Turing machine such that..."?

I just meant "any function you can write in the programming language you're considering". As robinhouston points out, not all functions will be definable, and "Turing-computability" is a bit vague when talking about functions that take other functions as arguments (since TMs operate on bitstrings, so how you encode functions becomes relevant). Constructive mathematics studies which things are still definable/provable if you insist on computability; "constructible" and "computable" usually mean the same thing.

> I don't know why computer people's category theory always looks so foreign to me. Sometimes I feel like we're in completely different worlds with vaguely similar-looking language. Category theory for me was mostly about homological algebra, but I don't think computer people care very much about the snake lemma or chasing elements across kernel and cokernel diagrams.

Yes. Category theory is a very general framework, and different bits of it become relevant depending on what you're studying. Although there are sometimes deep connections between unexpected regions, such as between computation and topology; I don't really understand that one myself.