5 ms·
This was very interesting. As a mathematician with no comp-sci type knowledge, my only understanding of inheritance is the "is a" rule. Using this, I realized
by quantdev 9y ago
This was very interesting.
As a mathematician with no comp-sci type knowledge, my only understanding of inheritance is the "is a" rule. Using this, I realized that a subtype of the set of functions from Dog to Dog must be a set of functions such that each function could be treated as a function from Dog to Dog under an appropriate restriction. This would be the only way for such a set to satisfy what felt like the "is a" inheritance rule.
In other words, a set of functions from A to B where Dog is contained in A and B is contained in Dog would be a subtype of the set of functions from Dog to Dog. So Animals -> Greyhound works.
- jordigh 9y agoCan you figure out what the functor is? As another mathematician, if they're saying "contravariant" I expect to see something like a Galois functor. This kind of looks like a pullback or an evaluation functor, but I can't even see the categories it might be between. Is it the Hom functor?
- rntz 9y agoSee 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 ago