4 ms·
Central to his teachings is the view that things are ‘empty’ (sunya). This does not mean that they are non-existent; only that they are what they are because of
by tel 13y ago
Central to his teachings is the view that things are ‘empty’ (sunya). This does not mean that they are non-existent; only that they are what they are because of how they relate to other things.
Immediately I thought of Category Theory as this statement is a not terrible expression of what CT tries to teach. I'll immediately recommend the paper Numbers Can Be Just What They Have To (http://www.cwru.edu/artsci/phil/NumbersCanBeJustWhattheyHaveTo.pdf http://www.cwru.edu/artsci/phil/NumbersCanBeJustWhattheyHave...) for more exploration.
Briefly, while CT is usually "bootstrapped" off having a notion of objects and their relations, it becomes quickly obvious that focusing on the objects themselves is useless—they are given no emphasis in CT and thus wither away to being nothing at all. Instead, absolutely every interesting property of the objects must be expressed in the relations they take with other objects.
This is formalized in the Yoneda Lemma which, in a not terrifically generalized form, can be written
forall a . (forall r . (a -> r) -> r) <-> a
which is to say "the collection of all ways to relate an object to other objects is isomorphic to the object itself".
So what's the point? Well, as the paper linked above suggests, sometimes the "intrinsic nature" of things makes them very difficult. We'd often like to equate two things which "ought to be the same" but aren't because their intrinsic nature differs. If you work in standard mathematics (set theory) you run into this problem because everything is described as having an intrinsic nature derived from sets. If you work in CT-based math you have no such issue because objects fail to have intrinsic natures altogether. They only have their "extrinsic" natures, their relations to other things.
- wfn 13y agoAhh, very nice. While at it: here's a very nice etymological explanation of why the Ubuntu-Yoneda lemma is called the Ubuntu-Yoneda lemma: https://golem.ph.utexas.edu/category/2013/03/spivak_on_category_theory.html#c043578 https://golem.ph.utexas.edu/category/2013/03/spivak_on_categ...
- tel 13y agoHaha! That's great! I'm going to keep that in mind from now on.
- dietrichepp 13y agoHaskellers may recognize (a -> r) -> r as a way to represent "a"... you'll see that type signature in more than a few libraries.
- tel 13y agoNot without the forall!
- dietrichepp 13y agoHaskell has implicit forall.
- tel 13y agoSorry, not to imply you weren't aware of the fact but instead to be completely clear. Taken as an cutout of the code I wrote it might seem as though you intentionally removed the forall.
- gohrt 13y agoFor what purpose? Surely the type checker doesn't recognize the equivalence. a1 :: a r1 :: r f :: a -> r f a1 = r1 b :: (a -> r) -> r b f = f a1 -- == r1 but `a f` is ill-typed. m :: a -> (a -> r) -> r m a1 f = f a1 -- m === (flip ($)) === (flip id) So it appears that `(a -> r) -> r` is a "co-value" that can be applied to a function (resulting in the application of the function to the underlying vale of type `a`, dual to the usual situation where functions are applied to values.
- tel 13y agoThis is pretty much exactly correct. The common terminology is that `forall r . (a -> r) -> r` is the Continuation Passing Style transformed version of `a`. At the end of the day, `CPS a` is useful whenever CPS is, but also more often. sometimes you see CPS (a.k.a. Church-encoded) forms of values in Haskell in really tight inner loops as the compiler can optimize them better. You also see a variant of it occurring in Free monad structures because it allows you to re-associate the binds to make them much more efficient. You also see it sometimes when making monads over categories other than Hask—it lets you pretend you're working with a Hask monad (and thus use do notation) for a while and only "pass through" the real category at fixed points in time. This lets you, for instance, write a monad for Set even though normally you couldn't due to the need for the Ord constraint.
- michaelfeathers 13y agoThis reminds me of Alan Kay's assertion that messaging is more important than objects in OO. I know that when I design, I see the interactions first - they define the objects. If names from the domain fit - fine. Otherwise, invent new names.
- e12e 13y ago(It also reminds me of Alan Kay describes differential functions)
- tel 13y agoI like to notice it as well as being a concise statement of the heart of the relational model. Ultimately, the things stored in your database are evidence of connections between other things, not the things themselves. Which is a good hint at the weight of the Object-Relational impedance problem, too.
- tel 13y agoOh, and generally, Rel, the category of relations is really interesting in its own right!
- SilasX 13y ago>which is to say "the collection of all ways to relate an object to other objects is isomorphic to the object itself". That reminds me of the time someone explained attributes in terms of relationships, using Magic: The Gathering as an example. In MtG, you have a player's creatures attacking the other player. Some of the flying ability, which means they can only be blocked by flying creatures. You can express that as "may only be blocked by creatures with this ability". There are also (a few) creatures can that can only be blocked and can only block flying creatures (which is not as good as flying), which you can express as "my only block or be blocked by creatures with the ability A", where A is the self-referential description of flying. I imagine you can stack it further and replace "player", "attack", and so on with some other relational/self-referential definition.
- e12e 13y agoHaving never really looked at Category Theory (having been convinced by a series of terrible writings by Haskell fanatics that nothing useful comes from studying it ;-) -- this is a beautiful teaser shining some light on why it might be useful for type theory in general (and as applied to computation in particular). So thank you for that! (And I do mean this comment, I'll be sure to look at the paper too -- but you managed to capture something that enticed my curiosity, which is a great thing)
- tel 13y agoCategory Theory and Type Theory end up feeling like the exact same subject viewed through different leneses. Bob Harper calls this concept Trinitarianism throwing Logic in as the third arm. I highly recommend studying Category Theory if you're interested in those kinds of topics. I think it's wonderfully enlightening for programming (although standard disclaimed applies that it's not necessary for programming). I recommend that paper, and I also recommend reading Conceptual Mathematics by Lawvere and Schanuel. It's easily my favorite book for getting into "how to think with CT".
- snowwrestler 13y agoThis reminds me of the holographic theory in physics which says (I am not a physicist, so layman's summary) that the information in a sphere of space can be completely represented on the surface of the sphere. If we think of that surface as its "interface" of relationship to the rest of the universe, it sounds very similar to: > "the collection of all ways to relate an object to other objects is isomorphic to the object itself".