5 ms·
See my other comment about co/contravariance as monotonocity/antimonotonicity. Since monotonicity is just functoriality when your categories are posetal, covari
by rntz 9y ago
See my other comment about co/contravariance as monotonocity/antimonotonicity. Since monotonicity is just functoriality when your categories are posetal, covariance is a special case of functoriality.
More generally, you can see
f(x) = Int -> x
g(x) = x -> Int
as, respectively, co- and contra-variant endofunctors on the category whose objects are types and whose arrows are definable functions in your programming language. And they're both just special-cases of the internal hom functor,
hom : C^op * C -> C
hom(x,y) = x -> y
- jclulow 9y agoYou keep using the word "just" in what feels like an unusual setting.
- rntz 9y agoI use "just" to mean "exactly"; I say "X is just Y" to mean "X is exactly Y; when you have Y, you have X and vice-versa". I guess it might be kind of off-putting, because "just" implies the connection is boring or obvious, which is not what I mean to say.
- jordigh 9y agoWow, that's a new word, "posetal". Does that mean "can be partially ordered"? What is "Int"? Integers? Integral? Int... ernal? ... types? What's with the notation, anyway? Why use "<:" instead of "<" like you would for any other transitive anti-symmetric relation? "Anti-monotone" is weird language. I would say "monotone" in general and "increasing" or "decreasing" in particular. 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. 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? What is a definable function? Are some functions not definable? Is it something like "there exists a Turing machine such that..."? 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.
- gsg 9y agoBecause S <: S in most (all?) type systems with subtyping.
- jordigh 9y agoThen use \leq, like any other reflexive, antisymmetric, transitive relation.
- robinhouston 9y agoA posetal category has at most one arrow in each homset – i.e. it’s a poset dressed up as a category. A definable function is one that can be defined in the programming language in question. There's a lot more to definability than Turing machines, when you consider higher types: that is, types whose domain is a function type. John Longley has written on this extensively.
- jordigh 9y agoThanks. Is there something to read that puts all of this together, starting from a common base? I really don't know where to start.
- robinhouston 9y agoI know what you mean about not knowing where to start! I think “all of this” is roughly what theoretical computer scientists call “Theory B”, or at least a large chunk of it, and where to start depends on which specific things you find most interesting. Benjamin Pierce’s _Types and Programming Languages_ is a relatively accessible introduction with an emphasis on types, but of course it’s just an overview of a pretty large research area.
- fmap 9y ago> 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. Well, another way to think about it is that we are using the same language to talk about very different things. For example, in homological algebra you are always working in (at least) a pointed category. In computer science a lot of the things we are interested in are already reflected in the partial order induced by a category (i.e., subtyping). If your category has a zero object the latter is trivial and so we're pretty much never looking at pointed categories.