Comment by tel | Hacker News Reader

Comment by tel | Hacker News Reader

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/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.

This 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".

This 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.

(It also reminds me of Alan Kay describes differential functions)

I 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.

Oh, and generally, Rel, the category of relations is really interesting in its own right!

>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.

Ahh, 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_categ...

Haha! That's great! I'm going to keep that in mind from now on.

Having 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)

Category 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".

Haskellers may recognize (a -> r) -> r as a way to represent "a"... you'll see that type signature in more than a few libraries.

Not without the forall!

Haskell has implicit forall.

Sorry, 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.

For 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.

This 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.

I recognise it as the type of continuation returning something of type a. Also, if you instantiate r to Void then

((a -> Void) -> Void) <-> a

is just double negation elimination.

Am I getting sidetracked or does this line go somewhere, tel?

You're totally correct that double-negation elimination is a specialization of the CPS transform which is a specialized form of Yoneda. Yoneda is more general and exists more often than CPS transforms do, though.

    cps : a -> (forall r . (a -> r) -> r)
    cps a = \f -> a f

    cps' : (forall r . (a -> r) -> r) -> a
    cps' f = f id

It's interesting to examine double negation elimination in constructivist logic since it doesn't hold there. In particular, we can easily write the backward direction

    bck : a -> ((a -> Void) -> Void)
    bck = cps a

but since we've now specialized `forall r` to `Void` we can no longer come back. This demonstrates (1) that the pure CPS'd version is more general than DNE and (2) proof by contradiction is non-constructive.

Typo: `bck` should obviously be

   bck = cps

Reply on news.ycombinator.com