Hacker News new | past | comments | ask | show | jobs | submit login
Compiling to Categories (2017) [video] (youtube.com)
84 points by espeed on Oct 27, 2018 | hide | past | favorite | 6 comments



This is a big breakthrough. You're getting multiple correct programs from a single expression by "instantiating" it over multiple formal Categories. Implementing new categories is pretty easy.

It can be seen as a generalization of monads and "semiring programming".

I kinda backed into this while writing a type-inferencer for Joy PL[1] (Joy expressions are already in point-free form.) The inferencer and the interpreter wound up being very similar, and I realized I had effectively implemented two categories (kinda): the interpreter evaluates a Joy expression in the Cat of values, while the inferencer evaluates the same expression in a Cat of stack effect descriptions.

So the same Joy expression computes values or infers types depending on which interpreter/category you choose to run it over. And, again, implementing a new category is brief and easy.

[1] http://joypy.osdn.io/notebooks/Types.html#hybrid-inferencer-...


I've been watching this stuff with great interest for a while now. Glad to see it's getting press here. Conal also has a paper on using this approach for automatic differentiation.

https://www.youtube.com/watch?v=MmkNSsGAZhw

http://conal.net/papers/essence-of-ad/

I've been playing around with his approach. It's super cool.

http://www.philipzucker.com/reverse-mode-differentiation-is-...

http://www.philipzucker.com/approximating-compiling-categori...


Chris Heunen and cols. have thought about a workaround to make probabilistic categories cartesian closed, and then Lambek translation from CCC to simply typed lambda calculus should apply, so Elliot machinery should also enable to express probablistic problems in Haskell terms.

[1] https://arxiv.org/abs/1701.02547


Conal Elliot was new to me, and he has great material! To cycle back to a recent good post: https://news.ycombinator.com/item?id=18306860

(comments there had this video posted as well)


I've been skeptical about the utility of category theory in software development, but this is pretty interesting stuff.

The source code for the programs he's talking about: https://github.com/conal/concat





Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: