[HN Gopher] RZK: Experimental proof assistant for synthetic [?]-...
___________________________________________________________________
RZK: Experimental proof assistant for synthetic [?]-categories
Author : adamnemecek
Score : 51 points
Date : 2023-09-28 16:41 UTC (6 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| skulk wrote:
| From 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. 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-...
|
| 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#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 wrote:
| 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-Lof type theory with type-in-type.
| xavxav wrote:
| wow that's really cool, I wonder what the essential
| difference is between type-in-type and other classic "nice"
| inconsistencies in type theories. It seems like it's "almost"
| consistent.
| skulk wrote:
| In this context, what do you mean by "normal terms"?
| gylterud wrote:
| Type theories usually come with a reduction relation on
| terms. It computes things like b-reduction for function,
| inserting arguments into function bodies, computes
| projections out of tuples, etc
|
| A normal term is one where no further reductions can be
| made. Without type-in-type you can prove that all terms can
| be reduced to a normal form. With type-in-type some terms
| normalise while other diverges.
|
| In fact, using type-in-type you can define the fixed point
| operator and do general recursion!
| riskable wrote:
| 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 wrote:
| 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-c...
| electrozav wrote:
| I didn't read it as a complaint, more of a humorous
| observation. Either way, there's no need to get aggressive
| onto someone that hasn't figured it out yet.
| danidiaz wrote:
| 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
|
| In the first part of this video Cedric Villani gives (in
| French) a nice explanation of the distinction:
| https://youtu.be/xzVk56EKBUI?t=258
|
| Edit: an English explanation, also by Villani:
| https://www.youtube.com/watch?v=AIrLXbwyYXQ
| hkopp wrote:
| 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.
| Loq wrote:
| 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.
| qsort wrote:
| I majored in CS and followed two graduate level courses on
| category theory. If it's any consolation I have no idea either.
| vjk800 wrote:
| 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 wrote:
| 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.
| ftxbro wrote:
| 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!
| hkopp wrote:
| 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 wrote:
| Actually, category theory, type theory, _and_ proof theory.
| staunton wrote:
| 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 wrote:
| > 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.
| [deleted]
| jlokier wrote:
| > HN has a fetish for both functional programming and cat
| theory
|
| Cat theory is something else:
| https://news.ycombinator.com/item?id=37685885
| carapace wrote:
| > 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/
| Loq wrote:
| 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 wrote:
| 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?
| throwaway17_17 wrote:
| I would argue that the last 30 years (if you arbitrarily
| begin at Moggi's paper on Monadic computation). Have shown
| ample impact of category theory on programming language
| theory and type theory more generally. Additionally, there
| are earlier work on the semantics of programming languages
| dating to the early 80's with strong category theory roots.
| There is a large body of work (I'm on mobile and don't have
| links) that uses category theory to backstop the
| development of algorithms and generic code solutions for
| all types of algebraic data types and container types for
| instance.
|
| There is a thriving 'school' of computer science that views
| category theory as the third leg of the category theory,
| type theory, proof theory triangle that forms their basis
| for all computer science. This is very evident in the CS
| department at Carnegie-Mellon. If you are interested I'd
| recommend checking the backlog of lecture videos and
| presentations at the Oregon Programming Language Summer
| School program.
| Loq wrote:
| Turing award winner Dana Scott already mentions
| categories in his work on models for the untyped lambda-
| calculus, for example in his 1971 monograph on
| _Continuous Lattices_ , which set the foundations of
| domain theory. Moggi monads came about, in parts, as a
| way of understanding domain theoretic constructins
| better.
| wk_end wrote:
| 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 wrote:
| 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
| Loq wrote:
| You could look at the papers being published in conferences
| like POPL, LICS, PLDI and ICFP.
|
| The theory of (Moggi) monads and monad transformers has
| been influencing modern programming (and libraries) very
| heavily (e.g. all of Haskell, Scala's ZIO vs Cats, Rust
| approach to returning errors). Most modern programming
| language research engages in some form or other with linear
| types (and its relatives, like affine) and they come from
| Girard's linear logic. Both (Moggi) monads and linear logic
| are heavily influenced by their inventors learning of
| category theory. So I'd say, whenever you program in a
| modern language or use modern library design, you
| (indirectly) stand on the shoulders of many giants. Some of
| those giants were category theorists.
|
| Interestingly, what I'm beginning to detect is an influence
| of computer science on category theory, if only because we
| want to verify abstract maths in automated tooling.
| wk_end wrote:
| While technically there's a relationship between category
| theory and substructural logics (of course there is,
| category theory is general enough that there's a
| relationship between it and everything), they don't
| really strike me as having that much to do with it
| directly - they're a fairly straightforward extension
| (restriction) of typical presentations of constructive
| logic. And I wasn't aware that e.g. Rust picked up its
| type system via exposure through category theory. Is
| there a source for that narrative?
| Loq wrote:
| > _Is there a source for that narrative?_
|
| Girard mentions the connection with categories all the
| time.
|
| For example in "Proofs and Types" he proves various
| theorems along the lines of: the sub-category of
| coherence spaces and stable maps (one of the main models
| that LL was developed for) induced by some LL fragment is
| cartesian closed category (IIRC). I think he developed LL
| in parts by fine-tuning it, until all the categories
| induced as models of fragments of LL have nice
| categorical properties. (To the extent that is possible.)
| When I was a PhD student, my supervisor suggested that I
| learn category theory to understand linear logic. (Not
| sure, in retrospect, that was the best course of action,
| but that was my trajectory)
| Loq wrote:
| > _Is there a source for that narrative?_
|
| Rust's types evolved over many years. Rust used to have
| _" typestate"_ for example. I had discussions with
| Graydon Hoare around 2011-ish about session types (which
| are linear). It struck me that Hoare knew exactly what I
| meant with the term. More generally, linear typing was
| just "in the air" in the early 2000s: you could not been
| serious in programming language design without being
| aware of linearity. Linearity was all over the research
| literature. Hoare was clearly very knowledgable in
| programming language research.
| uxp8u61q wrote:
| 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 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 wrote:
| Category theory is not the definition of categories.
| empath-nirvana wrote:
| I genuinely think it's because of people trying to understand
| WTF a monad is.
| downvotetruth wrote:
| 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 wrote:
| 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.
| armchairhacker wrote:
| Is the type system more or less complicated than Agda's?
___________________________________________________________________
(page generated 2023-09-28 23:01 UTC)