5 ms·

RZK: Experimental proof assistant for synthetic ∞-categories

61 points by adamnemecek 3y ago

hkopp 3y ago
I have studied math and was in some lectures about category theory. I still don't get what the project is about and that fact intrigues me.
- qsort 3y ago
  I majored in CS and followed two graduate level courses on category theory. If it's any consolation I have no idea either.
- Loq 3y ago
  It's just a theorem prover. Like every theorem prover it has a logic that you use for stating propositions, and proving theorem. The logic is a specific logic that is closely related to HoTT.
armchairhacker 3y ago
Is the type system more or less complicated than Agda’s?
vjk800 3y ago
Can someone explain to me why there are so many category theory posts in HN? To me it's just a pretty obscure branch of mathematics and there are almost no posts about any of the more popular branches of mathematics.
- whatshisface 3y ago
  Because it's perhaps the only intersection of: - Large research area - Definitions you can comprehend without a math background - Extremely vague applications so that there's no area in which it definitely doesn't apply. I think the hype, which has lasted for a decade now, is a result of there being a lot of smart people in different fields who are interested in math research, but not so interested they're going to catch up to whatever the Langlands program is about.
- hkopp 3y ago
  I think it is due to the homotopy type theory book. There is an elegant connection between category theory and type theory. I guess most of the people submitting category theory to hacker news (or any graduate math) just do it to flex and seem clever.
  - lo_zamoyski 3y ago
    Actually, category theory, type theory, and proof theory.
- staunton 3y ago
  HN is dominated by computer science people. Category theory is related to functional programming (e.g. Lisp), which academic computer scientists tend to like. Proof assistants are related to verifying correctness of software, which many computer scientists (especially the nerds, counting myself) like because it lets you dreem of a world that's not so messy (or at least of conquering the mess that it is in a small closed domain).
  - mathisfun123 3y ago
    > which academic computer scientists tend to like citation please? there's one guy in my department (one of the best theory departments in the US) that contributes to sml and that's about it as far functional goes. a less charitable/more accurate response to gop's question is: HN has a fetish for both functional programming and cat theory. there's even another response here that captures the sentiment beautifully: > I have studied math and was in some lectures about category theory. I still don't get what the project is about and that fact intrigues me.
    - jlokier 3y ago
      > HN has a fetish for both functional programming and cat theory Cat theory is something else: https://news.ycombinator.com/item?id=37685885 https://news.ycombinator.com/item?id=37685885
    - deleted 3y ago
      [deleted]
  - deleted 3y ago
    [deleted]
- downvotetruth 3y ago
  The Cartesian closed category's internal language is simply typed lambda calculus that has equivalent expressive power to combinatory logic where the y combinator was originally defined.
  - btilly 3y ago
    Note that the name "Y Combinator" was intended to appeal to a specific kind of hacker. A kind that was likely interested in functional programming, Lisp, and Paul Graham. Which was to say the kind of person that Paul Graham wished to convince to start startups with Y Combinator. And Hacker News was started as a discussion site to attract that kind of person here to where they would all become aware of each other, aware of Y Combinator, and aware of the opportunities to have from starting startups. The community of people here expanded out from that core. But category theory is pretty close to that original core, and so it isn't a surprise that it gets more attention here than elsewhere.
- uxp8u61q 3y ago
  A pretty obscure branch of mathematics? You've got to be kidding me. I don't understand HN's fetish for category theory either, and I find it rather weird - I'll refrain from even less charitable words. But as an actual professional mathematician... no, it's not an obscure branch of mathematics. You don't believe me? Read the ICM proceedings https://www.mathunion.org/icm/proceedings https://www.mathunion.org/icm/proceedings and count how many times the words "category" or "functor" appears. And notice something very special, too: you'll find articles that are not about category theory per se, and that will still mention categories. And you know what? They don't even explain what they are. You know how that can be? Categories are so pervasive in mathematics. You wouldn't write an article for the proceedings and explain what a group or a vector space is, would you? Well, same for categories. It's a basic (in the original sense of the word) part of mathematics.
  - bmacho 3y ago
    Category theory is not the definition of categories.
    - uxp8u61q 3y ago
      Uh?
      - bmacho 3y ago
        They use the word "category" instead of set, and the word "functor" instead of homomorphism. Category Theory is still very-very obscure, with little to no connection to the rest of mathematics.
        uxp8u61q 3y ago
        No, and no.
        Twey 3y ago
        I think this is a rather peculiar comment — category theory is interesting precisely _because_ it's closely connected to other branches of mathematics, and can be used as a lingua franca to translate concepts and discoveries between them.
- Loq 3y ago
  Category theory has been extremely influential in computer science, primarily because a (maybe the) prototypical idealised programming language (the simply typed lambda-calculus) is at the same time, a logic and a convenient syntax for cartesian closed categories (= basically the nicest, most well-behaved kind of category (which is, in turn, a foundation of topoi, a generalisation of the essence of all logics)). The trias gives extreme scope for technology transfer between mathematics, logic and programming.
  - bmacho 3y ago
    Any source for that? I don't think that category theory has even a minuscule influence on computer science. Type theory? Sure. Logic and model theory as well. Set theory? Number theory? Heck, even geometry is used for dozens of algorithms, not related to geometry (convex optimizing in an n dimensional space, Hamming distance, abstract convex geometry etc). But category theory? Do you have any influential papers or books in mind?
    - wk_end 3y ago
      The Haskell community was, quite clearly, heavily influenced by category theory. Monads (as a programming tool) fell out of that, and I suspect this directly influenced the treatment of async in Javascript (and elsewhere). I do think "extremely influential" is overstating it. Outside of that, plus some niches of niches of academic CS, I can't really think of any other places where category theory is particularly important.
      - bmacho 3y ago
        I am not sure that it influenced async in javascript. But the earliest monad paper I found in ~2 minutes of googling [0] even uses natural transformations which in my opinion counts as using CT. [0] Eugenio Moggi Computational lambda-calculus and monads (1989) https://www.cs.cmu.edu/~crary/819-f09/Moggi89.pdf https://www.cs.cmu.edu/~crary/819-f09/Moggi89.pdf
        3y ago
- empath-nirvana 3y ago
  I genuinely think it's because of people trying to understand WTF a monad is.
- ftxbro 3y ago
  My theory is that it's a kind of math that LLMs can do. Not that LLMs are necessarily doing it, but the same thing that makes it easy for LLMs also makes it easy for certain people. They can repeat words and phrases that they hear, and sometimes even rearrange them into new forms! One time some category theory guys were struggling with something and it was equivalent to topological sort in computer science. But the way they were failing at solving it sounded much more impressive!
- carapace 3y ago
  > It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/
riskable 3y ago
This is the URL I'm sending people to when I want to point out just how far domain-specific gibberish can go. Or just to mess with people... "I was looking for an experimental proof assistant for synthetic ∞-categories and stumbled across this awesome project..." "It's wicked cool! It uses a version of second-order abstract syntax which is great for lambda extraction." The project description sounds like something that MIT automated gibberish research paper generator would come up with.
- mathisfun123 3y ago
  what is the substance of this complaint? if i pull the API for django or react or ...anything else, how much should i be expected to understand without any prior exposure? how is "domain-specific gibberish" any different? you make up words to represent groups of other words in order to capture concepts. it's literally just how language works. let me translate for you: proof assistant: program that checks your work (writing a proof) and helps you find new proofs. synthetic: math where the axioms "represent" the objects instead of the other way around (they're "synthesized" from the objects) 1-category: a collection with objects and functions between them 2-category: a collection with objects, functions between them, and functions between those functions (called homotopies) k-category: you get the idea ∞-category: the limit as k -> ∞ second-order abstract syntax which is great for lambda extraction: syntax specifically suited for this kind of stuff and you know what? even though i am not a category theorist i was able to figure this out. you know how? i quickly skimmed the "docs" https://ncatlab.org/nlab/show/synthetic+%28infinity%2C1%29-category+theory https://ncatlab.org/nlab/show/synthetic+%28infinity%2C1%29-c...
  - danidiaz 3y ago
    I'm not a mathematician, but I feel the "syntethic"/"analythic" distinction in mathematics is an interesting and useful concept. "In modern mathematics, an analytic theory is one whose basic objects are defined in some other theory, whereas a synthetic theory is one whose basic objects are undefined terms given meaning by rules and axioms"—Michael Shulman In programming terms, I guess "synthetic" mathematics feels a bit like programming to an abstract interface. https://ncatlab.org/nlab/show/synthetic+mathematics https://ncatlab.org/nlab/show/synthetic+mathematics In the first part of this video Cédric Villani gives (in French) a nice explanation of the distinction: https://youtu.be/xzVk56EKBUI?t=258 https://youtu.be/xzVk56EKBUI?t=258 Edit: an English explanation, also by Villani: https://www.youtube.com/watch?v=AIrLXbwyYXQ https://www.youtube.com/watch?v=AIrLXbwyYXQ
skulk 3y ago
From https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction.rzk/#soundness https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction... > rzk-1 assumes "type-in-type", that is U has type U. This is known to make the type system unsound (due to Russell and Curry-style paradoxes), however, it is sometimes considered acceptable in proof assistants. And, since it simplifies implementation, rzk-1 embraces this assumption, at least for now. I do this too (in my HoTT-book-inspired proof-checker)! I do plan on eventually implementing a hierarchy of universes but it doesn't seem to be a problem to let U be of type U. I wonder where the first practical issue comes up when you allow this. --- After writing this comment, I decided to put it up on GitHub. Here is the entire source code of my proof-checker as well as some of the theorems from the HoTT book: https://github.com/sid-code/metalogic/blob/main/dts.org https://github.com/sid-code/metalogic/blob/main/dts.org. It was never meant to be used or even read by anyone else, but here it is. Here is where the universe is defined (unsoundly): https://github.com/sid-code/metalogic/blob/main/dts.org#the-universe https://github.com/sid-code/metalogic/blob/main/dts.org#the-... To see the theorems, scroll down past the machinery to the `(env-define-checked)` calls. Here is the proof that multiplication of natural numbers is associative: https://github.com/sid-code/metalogic/blob/main/dts.org#associativity-of-multiplication https://github.com/sid-code/metalogic/blob/main/dts.org#asso.... There is no type inference, so it's pretty gross. I think it's pretty cool how little you need to actually have a working proof-checker.
- gylterud 3y ago
  Interestingly, even thought type-in-type is inconsistent, there are no normal terms of the “empty” type. So, if you restrict to normal terms you do not get full explosion. There are however types A such that both A and not A have normal terms. It is just that if you combine them with modus ponens the term diverges. Another cool thing is that type-in-type is inconsistent, but has models. In particular, Palmgren constructed a model, based on domain theory, of Martin-Löf type theory with type-in-type.
  - skulk 3y ago
    In this context, what do you mean by "normal terms"?

61 points by adamnemecek 3y ago

I have studied math and was in some lectures about category theory. I still don't get what the project is about and that fact intrigues me.

qsort 3y ago
I majored in CS and followed two graduate level courses on category theory. If it's any consolation I have no idea either.
Loq 3y ago
It's just a theorem prover. Like every theorem prover it has a logic that you use for stating propositions, and proving theorem. The logic is a specific logic that is closely related to HoTT.

armchairhacker 3y ago

Is the type system more or less complicated than Agda’s?

vjk800 3y ago

Can someone explain to me why there are so many category theory posts in HN? To me it's just a pretty obscure branch of mathematics and there are almost no posts about any of the more popular branches of mathematics.

whatshisface 3y ago
Because it's perhaps the only intersection of: - Large research area - Definitions you can comprehend without a math background - Extremely vague applications so that there's no area in which it definitely doesn't apply. I think the hype, which has lasted for a decade now, is a result of there being a lot of smart people in different fields who are interested in math research, but not so interested they're going to catch up to whatever the Langlands program is about.
hkopp 3y ago
I think it is due to the homotopy type theory book. There is an elegant connection between category theory and type theory. I guess most of the people submitting category theory to hacker news (or any graduate math) just do it to flex and seem clever.
- lo_zamoyski 3y ago
  Actually, category theory, type theory, and proof theory.
staunton 3y ago
HN is dominated by computer science people. Category theory is related to functional programming (e.g. Lisp), which academic computer scientists tend to like. Proof assistants are related to verifying correctness of software, which many computer scientists (especially the nerds, counting myself) like because it lets you dreem of a world that's not so messy (or at least of conquering the mess that it is in a small closed domain).
- mathisfun123 3y ago
  > which academic computer scientists tend to like citation please? there's one guy in my department (one of the best theory departments in the US) that contributes to sml and that's about it as far functional goes. a less charitable/more accurate response to gop's question is: HN has a fetish for both functional programming and cat theory. there's even another response here that captures the sentiment beautifully: > I have studied math and was in some lectures about category theory. I still don't get what the project is about and that fact intrigues me.
  - jlokier 3y ago
    > HN has a fetish for both functional programming and cat theory Cat theory is something else: https://news.ycombinator.com/item?id=37685885 https://news.ycombinator.com/item?id=37685885
  - deleted 3y ago
    [deleted]
- deleted 3y ago
  [deleted]
downvotetruth 3y ago
The Cartesian closed category's internal language is simply typed lambda calculus that has equivalent expressive power to combinatory logic where the y combinator was originally defined.
- btilly 3y ago
  Note that the name "Y Combinator" was intended to appeal to a specific kind of hacker. A kind that was likely interested in functional programming, Lisp, and Paul Graham. Which was to say the kind of person that Paul Graham wished to convince to start startups with Y Combinator. And Hacker News was started as a discussion site to attract that kind of person here to where they would all become aware of each other, aware of Y Combinator, and aware of the opportunities to have from starting startups. The community of people here expanded out from that core. But category theory is pretty close to that original core, and so it isn't a surprise that it gets more attention here than elsewhere.
uxp8u61q 3y ago
A pretty obscure branch of mathematics? You've got to be kidding me. I don't understand HN's fetish for category theory either, and I find it rather weird - I'll refrain from even less charitable words. But as an actual professional mathematician... no, it's not an obscure branch of mathematics. You don't believe me? Read the ICM proceedings https://www.mathunion.org/icm/proceedings https://www.mathunion.org/icm/proceedings and count how many times the words "category" or "functor" appears. And notice something very special, too: you'll find articles that are not about category theory per se, and that will still mention categories. And you know what? They don't even explain what they are. You know how that can be? Categories are so pervasive in mathematics. You wouldn't write an article for the proceedings and explain what a group or a vector space is, would you? Well, same for categories. It's a basic (in the original sense of the word) part of mathematics.
- bmacho 3y ago
  Category theory is not the definition of categories.
  - uxp8u61q 3y ago
    Uh?
    - bmacho 3y ago
      They use the word "category" instead of set, and the word "functor" instead of homomorphism. Category Theory is still very-very obscure, with little to no connection to the rest of mathematics.
      - uxp8u61q 3y ago
        No, and no.
      - Twey 3y ago
        I think this is a rather peculiar comment — category theory is interesting precisely _because_ it's closely connected to other branches of mathematics, and can be used as a lingua franca to translate concepts and discoveries between them.
Loq 3y ago
Category theory has been extremely influential in computer science, primarily because a (maybe the) prototypical idealised programming language (the simply typed lambda-calculus) is at the same time, a logic and a convenient syntax for cartesian closed categories (= basically the nicest, most well-behaved kind of category (which is, in turn, a foundation of topoi, a generalisation of the essence of all logics)). The trias gives extreme scope for technology transfer between mathematics, logic and programming.
- bmacho 3y ago
  Any source for that? I don't think that category theory has even a minuscule influence on computer science. Type theory? Sure. Logic and model theory as well. Set theory? Number theory? Heck, even geometry is used for dozens of algorithms, not related to geometry (convex optimizing in an n dimensional space, Hamming distance, abstract convex geometry etc). But category theory? Do you have any influential papers or books in mind?
  - wk_end 3y ago
    The Haskell community was, quite clearly, heavily influenced by category theory. Monads (as a programming tool) fell out of that, and I suspect this directly influenced the treatment of async in Javascript (and elsewhere). I do think "extremely influential" is overstating it. Outside of that, plus some niches of niches of academic CS, I can't really think of any other places where category theory is particularly important.
    - bmacho 3y ago
      I am not sure that it influenced async in javascript. But the earliest monad paper I found in ~2 minutes of googling [0] even uses natural transformations which in my opinion counts as using CT. [0] Eugenio Moggi Computational lambda-calculus and monads (1989) https://www.cs.cmu.edu/~crary/819-f09/Moggi89.pdf https://www.cs.cmu.edu/~crary/819-f09/Moggi89.pdf
      - 3y ago
empath-nirvana 3y ago
I genuinely think it's because of people trying to understand WTF a monad is.
ftxbro 3y ago
My theory is that it's a kind of math that LLMs can do. Not that LLMs are necessarily doing it, but the same thing that makes it easy for LLMs also makes it easy for certain people. They can repeat words and phrases that they hear, and sometimes even rearrange them into new forms! One time some category theory guys were struggling with something and it was equivalent to topological sort in computer science. But the way they were failing at solving it sounded much more impressive!
carapace 3y ago
> It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/

riskable 3y ago

This is the URL I'm sending people to when I want to point out just how far domain-specific gibberish can go. Or just to mess with people... "I was looking for an experimental proof assistant for synthetic ∞-categories and stumbled across this awesome project..." "It's wicked cool! It uses a version of second-order abstract syntax which is great for lambda extraction." The project description sounds like something that MIT automated gibberish research paper generator would come up with.

mathisfun123 3y ago
what is the substance of this complaint? if i pull the API for django or react or ...anything else, how much should i be expected to understand without any prior exposure? how is "domain-specific gibberish" any different? you make up words to represent groups of other words in order to capture concepts. it's literally just how language works. let me translate for you: proof assistant: program that checks your work (writing a proof) and helps you find new proofs. synthetic: math where the axioms "represent" the objects instead of the other way around (they're "synthesized" from the objects) 1-category: a collection with objects and functions between them 2-category: a collection with objects, functions between them, and functions between those functions (called homotopies) k-category: you get the idea ∞-category: the limit as k -> ∞ second-order abstract syntax which is great for lambda extraction: syntax specifically suited for this kind of stuff and you know what? even though i am not a category theorist i was able to figure this out. you know how? i quickly skimmed the "docs" https://ncatlab.org/nlab/show/synthetic+%28infinity%2C1%29-category+theory https://ncatlab.org/nlab/show/synthetic+%28infinity%2C1%29-c...
- danidiaz 3y ago
  I'm not a mathematician, but I feel the "syntethic"/"analythic" distinction in mathematics is an interesting and useful concept. "In modern mathematics, an analytic theory is one whose basic objects are defined in some other theory, whereas a synthetic theory is one whose basic objects are undefined terms given meaning by rules and axioms"—Michael Shulman In programming terms, I guess "synthetic" mathematics feels a bit like programming to an abstract interface. https://ncatlab.org/nlab/show/synthetic+mathematics https://ncatlab.org/nlab/show/synthetic+mathematics In the first part of this video Cédric Villani gives (in French) a nice explanation of the distinction: https://youtu.be/xzVk56EKBUI?t=258 https://youtu.be/xzVk56EKBUI?t=258 Edit: an English explanation, also by Villani: https://www.youtube.com/watch?v=AIrLXbwyYXQ https://www.youtube.com/watch?v=AIrLXbwyYXQ

skulk 3y ago

From https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction.rzk/#soundness https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction... > rzk-1 assumes "type-in-type", that is U has type U. This is known to make the type system unsound (due to Russell and Curry-style paradoxes), however, it is sometimes considered acceptable in proof assistants. And, since it simplifies implementation, rzk-1 embraces this assumption, at least for now. I do this too (in my HoTT-book-inspired proof-checker)! I do plan on eventually implementing a hierarchy of universes but it doesn't seem to be a problem to let U be of type U. I wonder where the first practical issue comes up when you allow this. --- After writing this comment, I decided to put it up on GitHub. Here is the entire source code of my proof-checker as well as some of the theorems from the HoTT book: https://github.com/sid-code/metalogic/blob/main/dts.org https://github.com/sid-code/metalogic/blob/main/dts.org. It was never meant to be used or even read by anyone else, but here it is. Here is where the universe is defined (unsoundly): https://github.com/sid-code/metalogic/blob/main/dts.org#the-universe https://github.com/sid-code/metalogic/blob/main/dts.org#the-... To see the theorems, scroll down past the machinery to the `(env-define-checked)` calls. Here is the proof that multiplication of natural numbers is associative: https://github.com/sid-code/metalogic/blob/main/dts.org#associativity-of-multiplication https://github.com/sid-code/metalogic/blob/main/dts.org#asso.... There is no type inference, so it's pretty gross. I think it's pretty cool how little you need to actually have a working proof-checker.

gylterud 3y ago
Interestingly, even thought type-in-type is inconsistent, there are no normal terms of the “empty” type. So, if you restrict to normal terms you do not get full explosion. There are however types A such that both A and not A have normal terms. It is just that if you combine them with modus ponens the term diverges. Another cool thing is that type-in-type is inconsistent, but has models. In particular, Palmgren constructed a model, based on domain theory, of Martin-Löf type theory with type-in-type.
- skulk 3y ago
  In this context, what do you mean by "normal terms"?