Blog » Intergalactic Telefunctors and Quantum Entanglement
Posted on 1234713995|%A: %d %B, %Y|agohover
In a previous article I argued against the pernicious Container Fiction. Some respondents have quite reasonably responded that this seems a bit pedantic; it may be true that e.g. a list is not really a container, but it's such a useful metaphor that only a pedant would insist on banning it.
Indeed it is a very useful metaphor, but the motivation for exposing it as a "pernicious" myth is not linguistic fascism, but rather pedagogical clarity. The Container Fiction is only pernicious insofar as it interferes with a clear understanding of the underlying abstraction it attempts to capture: the functor as a special kind of relation that enables communication between two different and mutually incomprehensible universes. This is bound to happen, since the container fiction is deeply embedded in the world of set theory, and the key to understanding Haskell is category theory, which is a whole nother thing.
The list is probably not the best example, since it involves a lot of complexity, what with the free monad and so forth. A simpler example would be a pair (a,b). This can obviously considered a kind of container, but as metaphors go a somewhat less pernicious image is the chemical compound. A chemical compound has different properties than its consituents; carbon monoxide (CO) is quite a different thing than carbon and oxygen. It's not a container of its constituents, it's their compound. The relation of (the denoted value) of "(a,b)" to its "components" a and b is similar. It's a mereological relation, not a containership relation.
But even that obscures the true nature of the functor (). The value denoted by "(a,b)" is not a compound, it is a primitive, whole, opaque value. (Disregard for the sake of argument whether it is dependent on the human mind.) The compound is the expression "(a,b)" itself.
My proposition is that a category theoretic explanation can be clearer and simpler than such metaphorical expositions, leading to a solid articulated intuition of the structural nature of functors without resorting to colorful metaphors. Well, maybe one, but it's arguably not a metaphor. A full exposition would take some very careful writing and a bunch of diagrams, but here's a sketch of how it would work.
Start with a, b, and (). Symbols 'a' and 'b' name things in a home universe; '()' is (the name of) an intergalactic "telefunctor" that relates the home universe to an alien universe of pair values. "(a,b)" takes two primitive values from home to a third primitive value in the alien universe. It doesn't convey a and b to the alien universe; rather, it entangles them. IOW, "(a,b)" is a kind of name or definite description of a value that is just as primitive and indivisible as the value denoted by "a" but that lives in an alien universe. We could say that "(a,b)" represents the quantum entanglement of a and b with the value denoted by "(a,b)". Call that value x. It lives in an alien universe; we know nothing about its internal structure, nor what it looks like in its universe, nor how it relates to other elements of its universe. But we do know something about how it relates to values in our home universe. We obviously know it is related - via () - to a and b together. But we also know, because of the way we define () - since this is just a brief sketch I omit this definition - we know that x is related to a and b individually. Our definition of () goes with two other definitions: fst (a,b) = a, and snd (a,b) = b.
Now we have defined the value of () purely in terms of how it relates things across intergalactic (ok, couldn't resist a metaphor) boundaries - morphisms. We could go further and show how a and b can also be defined as morphisms - after all, they're just names denoting values, and those values are just as opaque and unapproachable as the value of "(a,b)". Our knowledge of how all these things behave is expressed in terms not of what they are, but in how they relate. You can judge a man by his friends; you can understand mathematical values by their relations to other values.
A diagram might represent values as blackened circles. I believe this approach leads to a very clear, simple, and reasonably complete exposition. The metaphor of alien universes and intergalactic telefunctors could of course be dispensed with, but it does add color without introducing semantic distortion.
The real virtue of this approach becomes more clear when we complement the above exposition of the object component of a functor with a similar account of the morphism component that takes functions from one realm to functions in the alien realm. The pedagogical payoff is the realization that a functor allows us to use what we know about values in one realm to "manipulate" values in another realm. The best metaphor for the functor is neither containment nor mereology, but quantum entanglement.
Like this entry?
Leave a comment
Just realized that "quantum" is an excellent replacement for "value". So e.g. '3' denotes not a number but a quantum that we happen to name '3', or, the value of '3' is that quantum.
I don't think category theory is the key to understanding Haskell. A little bit of domain theory helps though.
And, btw, this gave me no insight to what you think a container is.
I'm not sure what you're looking for; at any rate I don't have anything fancy in mind, just anything that contains. A set being the canonical example. Does that answer your question?
So to me a container, C, is something that (very informally) has these operations
You can stick something into the container, and then you can get it out. Depending on the container it might be able to hold more than one item, etc.
So that means that 'Maybe Int' is a container for Int. The Maybe type constructor is strictly speaking not a container, since it's not even kind correct to say so. But it's convenient to talk about Maybe as a container anyway, since there's no real risk of confusion.
If that works for you, I would not argue against it. But I would object if you were to instruct newcomers by saying "this is what it really is". What you've described are not set operations, they're more like imperative operations on a set-like data structure. There's really only one operation involved in "containers", and that is membership. It's not even an operation, it's a predicate. You cannot "add" or "stick" a new element into a set; you can only form the union of two sets. Nor can you remove an element of a set; you can only ask if the element is a member of the set. "put C A" really means: form the set {C} and then take the union of {C} and A; "get c A" doesn't really mean much of anything; I suspect you mean something more like "member? c A". Sets are unordered; there is absolutely no way to select a specific element of a set; the best you can do is ask of that element is in the set or not.
Whether or not Maybe is a usefully thought of as a container really depends on who is doing the thinking. For many people that's fine and dandy, no problem. For others, not. Either way, technically, it is not a container. The predication "a isMemberOf (Maybe a)" is false, period.
Well, I wouldn't want to try to speak for augustss, but I don't see anything specifically imperative about his put/get example: I, at least, interpreted him to mean something that could be axiomatized algebraically, including including something along the lines of "a = get(put(a))" Well, writing it down I see that perhaps what you're getting at has to do with the lack of a key, although you didn't use quite the same type of operations he (augustss) indicated.
Regarding selecting things from a set, I understand what you're getting at … but if I know something in advance I suspect might be in a set, I can certainly see if it's in there, and if it is, I can then form the new set, as a predicate, which returns false for the thing in question and defers to the original predicate on everything else. This is only possible if I know what to look for in advance, but in a typed context it might be possible in principle (if not efficient) to enumerate the possibilities.
What i tell to beginners is "observe the types", "mind the types", "type is behavior", "the arrow is right associative", "the application is left-associative".
The more they are confortable with types, functionnal types, product types & sum types, the less the urge to perpetuate the object intuition.
We want them to abandon the objet-oriented thinking, but in my opinion it's not so much desirable to resort to alien scary words to exorcize the object conditioning.
Typically arrow and application should be powerful enough to instil the mind change.
Then let it mature long enough and some will eventually demand more.
- damien
I agree about alien scary words. I'm not sure I would use the intergalactic telefunctor as an explanatory device, although once you grok functors it's kind of amusing.
I'm also realizing, the more I get into it, just how conditioned my thinking was by set theory. I had learned Z pretty well, so I was thinking about everything in terms of straightforward ZF denotations. I'm beginning to think the learner should be warned at the beginning that notions of set theory will have to be not so much unlearned as relearned from a CT perspective.
Thanks,
gregg
Define functor (as in the categorical concept) formally.
A (covariant) functor is some morphism map with type (α→β) → (ϕ(α)→ϕ(β)) that obeys these two laws:
(initially, it really helps if you think that a functor lifts an item function to the container level)
For example the (,) bifunctor takes two identity morphisms idα and idβ and it gives you (fst,snd) as the identity for pairs.
The classical way would be to say (a,b) is some constructor invocation that returns a new object that accepts two destructors fst and snd.
The difference is the former ressembles a specification while the latter ressembles an implementation.
If you are a functional programmer chasing abstraction, then you are encouraged to go the categorical way. Also, lazyness implies that potentially any data is actually a function, that greatly favors the categorical point of view.
Thanks, but I was not asking for you to define it. My request still stands for Gregg.
I posted this in reply to the other post, but again, here is one formalization of the notion of a container, and if you don't like it, you need to confront it rather than dismiss it.
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.285
Post preview:
Close preview