9 ms·

Native Type Theory

116 points by gbrown_ 6y ago

acjohnson55 6y ago
Well, that paper escalated quickly! I've dabbled in enough category theory to have some inkling of the meaning of this, but not much. I've kind of given up on expecting an epiphany from this stuff that's applicable coding in a way that significantly changes my practice in any short period of time, but I'm still tempted by the feeling that the big revelation is just a couple concepts away.
- roenxi 6y ago
  It seems unlikely that there will be any profound insights from category theory on how to write code, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things. Category theory is likely to contribute by giving specialists a language they can use to communicate, and it seems likely to me that at some point general tools rooted in category theory will have some sort of interesting implication for testing and debugging. Taking Haskell for example; the language isn't anything to write home about but the type checking in the tooling enabled a big improvement in writing bug free code. So there is a probably a lot on offer for the sort of people who write tooling, and less on offer for everyone else.
  - pgustafs 6y ago
    “It seems unlikely that there will be any profound insights from logic on how to compute, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things.“
    - roenxi 6y ago
      It would be helpful if you fleshed that out a little, I'm curious about how you think insights from logic helps people program. I don't think I could deduce whether a developer knew or was ignorant of formal logic in a code review. Unless they give it away with a rather direct comment. Recognising that a programming language is equivalent to some mathematical construct is a very different thing from getting a practical insight about what decisions to make. My shirt is some sort of topological embedded space, but the tailoring as a field has not gained much practical insight from the study of topology. Although I would encourage any aspirations the tailors have might have to a broad education.
      - pgustafs 6y ago
        I was referring to the fact that computers themselves are the descendants of logicians — Church, Turing, von Neumann. Your argument above could have just as easily been used to attack Turing machines before the invention of the general purpose computer.
      - calhoun137 6y ago
        +1 for the request for a rephrasing. When Faraday was asked about what the practical use of his discovery of electromagnetic induction was, he famously replied, "what is the use of a newborn baby?" Which is how I read the OP
        pgustafs 6y ago
        Here’s another great quote along the same lines: “No one has yet discovered any warlike purpose to be served by the theory of numbers or relativity, and it seems unlikely that anyone will do so for many years.” GH Hardy 1941
  - GregarianChild 6y ago
    Category theorists have made this promise since the early 1990s, when the overlap between categorical methods and pure functional programming (think type theories) became clear. The really big win here was Moggi's discovery that monads neatly generalise many similar ideas in programming. (Moggi/Plotkin should have won a Goedel award for this!) This led to a great deal of activity towards generalising this to other forms of computation, in particular parallel computing (key problem: generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding). In my opinion, this has comprehensively failed to date, in the sense that (A) while you can express some parallelism in a way that can be read as a generalisation of cut-elimination / category theory, that is not surprising since (simplifying a great deal for brevity) category theory is a foundation of mathematics; but (B) when you express non purely functional computation categorically, you get extremely complicated formal systems that obscure the fundamental simplicity of what they abstract from and generally have only what they abstract from as actual model of the abstraction. Let's take Example 47 from the Native Type Theory paper: what exactly is the formal property the typing system induces? (The paper makes vague allusions to a "foreign function interface" with rho-calculus, but there is no published understanding of even the equational theory of rho-calculus. Why should I trust this paper?) What is the logic that the paper promises ("Native Type Theory gives provides a shared framework of reasoning")? What are the proof rules, so I can type them into Lean or Coq? Show me that they are better than the simple logics I get from looking at lambda-calculus operationally. Each abstraction has costs and benefits. As of 2021, the costs of categorical methods outside of pure functional languages outweigh their benefits. I worked in categorical methods for programming and changed the field, when I realised this.
    - siraben 6y ago
      > generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding How would you generalize the correspondence between cut-elimination and beta-reduction to cut-elimination and parallel composition, and what is meant by hiding here? I would be curious to know of relevant work in the area.
      - 6y ago
  - specialist 6y ago
    > profound insights from category theory on how to write code Sure. But as u/feniv hinted upthread, I'm also optimistic about the impact on language design (noodling). I too have a hobby toy language. For the type system, I just want to use the best available science. Hopefully something practical, easy to explain, simple to use, with good enough ergonomics. While type theory is really important, it's just not my area of interest, and I'd like to defer to the experts.
  - calhoun137 6y ago
    > It seems unlikely that there will be any profound insights from category theory on how to write code I strongly disagree with this. To me it does not seem "unlikely", quite the opposite. The reason I feel so strongly about this is that computer science is a subset of pure mathematics, its the part that deals with algorithms and computation. There are many questions in computer science which cannot be answered without an appeal to pure math (e.g., what is the best possible compression algorithm) All of computer science began as a result of the work of Hilbert on the foundations of logic[1]. This is what led to Turing's paper on Turing Machines. Since that time, mathematicians have done a lot of exciting work on foundations. Category theory has completely transformed the way we think about abstract mathematical objects; and type theory is very exciting in that it brings mathematics closer to a programming language which is compiled in the human brain and is done with pen and paper. It's seems to me very likely that in the future, code writing standards will change and get better, and will not remain the same. Towards that end, it makes sense that improvements will come from a better understanding of foundations, since that is where it all started. Curious for your thoughts? [1] https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:text=The%20system%20Hilbert%20asked%20for,than%20first%2Dorder%20Peano%20arithmetic.&text=Thus%20a%20satisfactory%20answer%20to,already%20believe%20PA%20is%20consistent https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:....
    - threatofrain 6y ago
      What has been your interest in category theory? How has category theory empowered your work?
      - calhoun137 6y ago
        My interest in category theory is just as a hobby and an amateur; but I have gone pretty deep reading lots of books and so on. To be fair, category theory has not empowered my work (in programming) at all.
        feanaro 6y ago
        I find category theory empowers my programming in the design step, much more so than when actually writing code. It enables me to find a more elegant design from the outset and be sure of its utility and elegance even before I program it.
- threatofrain 6y ago
  But category theory is very foundational theory. It would similarly be like learning set theory without further goals, which would be fine if you think of it as alternative Sudoku. As a foundational language it’s there to formalize mathematical objects, but that doesn’t mean people think in either set or category theory, as opposed to higher level objects in their domain.
  - acjohnson55 6y ago
    Totally agree. Just musing on my desire to fully understand this paper, but with the knowledge that all the steps to get there probably won't do much for me outside their own satisfaction. Which, admittedly, might be fun.
- calhoun137 6y ago
  > I've kind of given up on expecting an epiphany from this stuff that's applicable coding in a way that significantly changes my practice Same. It makes me kind of sad that pure math is not more helpful here! I think its possible that coding standards today are really high quality, and that any improvements are going to require a revolutionary paradigm shift in how we think about programming at an extreme level of generality. That's where pure math comes in, its a good place to shop around for new ideas, since we are kind of at a local maximum now in terms of best practices, imo. This is how I use math while coding: Instead of tinkering with numbers, just calculate the thing and get all the numbers right the first time. When trying to solve a problem, it's super helpful to have spent years proving theorems in pure math, it helped me compile programs in my head. When I am suuuuuuper stuck and need to figure out if what I am trying to do has already been done in math somewhere. When constructing an overall plan for a project, using abstract concepts in mathematics to properly anticipate the limits of what various implementations will be in order to pick the best one.
  - tsss 6y ago
    Unfortunately, I think quality simply isn't needed for all the web shops and trivial CRUD applications that most programmers work on.
- proc0 6y ago
  CT helps advance Denotational Semantics, so syntax is written closer to math syntax, which I think is approaching computation in a much more stricter way and therefore leveraging the "magic" of math. Of course the price is paid in complexity of the theory and learning curve to understand it, which kills its practicality.
- carapace 6y ago
  Have you seen "Compiling to categories"? > 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. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages. http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/
siraben 6y ago
A good introduction to categorical logic is [0], introducing the simply-typed lambda calculus along with the categorical semantics for each construction (cartesian closed categories). The later sections include topics mentioned in this article such as hyperdoctrines, categorifying quantifiers, and dependent types. [0] https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf
- 3PS 6y ago
  CMU also currently has a course in categorical logic [0]. Internally, the only prerequisite is a course in category theory. The course notes can be found at [1]. [0] http://mathieu.anel.free.fr/CLcourse.html http://mathieu.anel.free.fr/CLcourse.html [1] http://mathieu.anel.free.fr/mat/80514-814/Awodey-Bauer-catlog(2019).pdf http://mathieu.anel.free.fr/mat/80514-814/Awodey-Bauer-catlo...
chewxy 6y ago
I followed this until the part just slightly after "see how natural it is?" Then it's suddenly How to Draw an Owl. I don't follow the monoid part. Anyone can help elaborate?
- siraben 6y ago
  > Dependency is pervasive throughout mathematics. What is a monoid? It’s a set M, and then operations m,e on M, and then conditions on m,e. Most objects are constructed in layers, each of which depends on the ones before. Type theory is often regarded as “fancy” and only necessary in complex situations, similar to misperceptions of category theory; yet dependent types are everywhere. A monoid is (S,•,e): a set S equipped with a binary operation • : (S,S) -> S such that for all x, y, z in S, x•(y•z)=(x•y)•z, and an element e in S such that for all x in S, x•e=e•x=x. Examples of monoids include (String,concat,""), (int,0,+) and so on. One recurring theme in universal algebra and category theory is the notion of an algebra[0], in programmer terms it's like a module declaration. (see also F-algebra[1] which is heavily used in functional programming to formalize the notion of folding and more) Dependent type theory allows one to encode these algebras, e.g. encoding monoids and their laws in Coq's type system CoC[2]. Just like how ADTs in Haskell/OCaml and enums in Rust are comprised of a "sum of products", products and sums can be generalized in dependent types as well: Length-indexed lists via the dependent sum: Σn:ℕ.List(n) consists of dependent pairs ⟨n,l:List(n)⟩. Σn:ℕ.List(n) can be read as a function that takes a natural number n and returns a type List(n) Type-parametrized types: ΠS:Set.List(S) consists of dependent functions λS:Set.φ(S), ΠS:Set.List(S) can be read as a function that takes a type S and returns a type List(S) So to encode monoids in a dependent type theory using those dependent sums and products, we can just put the operations and laws into some big record, say Monoid:= ΣM:Set. Σm:M²→M. Σe:()→M. Π(a,b,c):M³.m(m(a,b),c)=m(a,m(b,c)). Πa:M.m(e,a)=a=m(a,e). Compare this to [2]! [0] https://en.wikipedia.org/wiki/Universal_algebra#Basic_idea https://en.wikipedia.org/wiki/Universal_algebra#Basic_idea [1] https://en.wikipedia.org/wiki/F-algebra https://en.wikipedia.org/wiki/F-algebra [2] https://gist.github.com/puffnfresh/11258181#file-monoid-v-L5 https://gist.github.com/puffnfresh/11258181#file-monoid-v-L5
  - siraben 6y ago
feniv 6y ago
Seems like this is an extension of the Curry-Howard-Lambek isomorphism [1] relating type theory, logic and category theory together. I find that to be one of the most beautiful results in computer science and have been working on a practical language built on the same principles for a while (A mix of Haskell, Prolog and APL in a python-like language) [1] https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence
- Tabzz98 6y ago
  Is there any online material on this language?
  - feniv 6y ago
    Not yet. I've specced it out, but still working on the implementation. Here's a hand-written example showing how you can specify the constraints to validate a Knight's tour. You can then enumerate over the types to get valid tours. https://gist.github.com/Feni/d819f120a7d179bc472c94df9471e600 https://gist.github.com/Feni/d819f120a7d179bc472c94df9471e60...
jimmyed 6y ago
I am a literal newbie to this field. How is this field related to logic?
- guerrilla 6y ago
  I suggest starting by looking up the Curry-Howard isomorphism.
- blovescoffee 6y ago
  How much of a literal newbie? Are you familiar with predicate logic / any formal logic? Are you familiar with any basic modern algebra like Group theory?
  - jimmyed 6y ago
    I was educated in the UK, so have a good grip on the highschool math there, but not much beyond that. I did try to plough thru SICP, that's a work in progress. Too little you'd say?
    - blovescoffee 6y ago
      Well it's too little to understand immediately but you can definitely come to grasp this stuff. There are a lot of mathy words here that do warrant their invocation but don't mean that the math is arcane. You seem like you're interested which is all that matters. I'm going to be slightly handwavey/generalize here but I think it may be helpful. Predicate Logic is the basic logic that humans think of when they think "logic." It's, if-this-then-that style thinking with only basic "tools". Predicates are statements that can lead to other statements, for instance the predicate "it's raining" could imply the predicate "I will wear a jacket." You can even combine predicates such as, if "I'm hungry" _and_ "I have food in the fridge" then "I will eat." Typically, we use symbols instead of sentences so it will look more like (A and B) -> C. Assuming you've done some programming, you're already used to predicate logic in the form of if-else statements. You've also been exposed to type theory. I think SICP is in scheme so types are a little bit hidden but if you've programmed any of the modern non-lisp languages i.e. Python, Java, C, etc. then you've seen types. Types are ints, floats, strings, etc. You know how you can add two numbers but you can't add a number and a string without special rules? (1+1 == 2 but "cat" + 1 == ???) Type theory concerns these rules and a bit more. A question that type theory helps answer is, what are we permitted to do with certain classes of objects? Once the blog post gets into dependent types, I think it becomes a bit tricky to pick up. Dependent types are types that "depend" on other information. For instance, we might have a type called array which is a sequence of numbers of any length. We might further have a dependent type called the PointTripleArray := Array<3> i.e. it's an array with 3 terms and they type of PointTripleArray is the dependent type. There are other more complicated ways to use dependent typing but I'll skip those. Honestly, I kind of understand the rest of the post but not well enough to start explaining here. I wish I could. I think this is enough to get you started reading and learning though.
calhoun137 6y ago
I really like this idea! I first got into type theory as a result of an answer by Carl Mummert to a question I asked on Math StackExchange[1]. I even wrote a blog post about it a year later[2]. Ever since then, I have considered type theory to be my favorite version of the foundations of math. I have often played around in theoretical foundations theory to discover as many connections as possible between foundations of math and computer science. That being said, I think the perspectives offered by set theory and category theory are extremely valuable, and that these three approaches compliment each other, and sometimes one is better than another for a specific purpose. This is the first time I had really seen the possibility to reformulate computer science to bring it closer to mathematics. How exciting! [1] https://math.stackexchange.com/questions/1519330/is-it-possible-to-formulate-category-theory-without-set-theory https://math.stackexchange.com/questions/1519330/is-it-possi... [2] https://medium.com/@calhoun137/a-programmers-way-of-thinking-about-sets-and-categories-3f10ef2fa72c https://medium.com/@calhoun137/a-programmers-way-of-thinking...
6gvONxR4sf7o 6y ago
This whole post is above my head, reminiscent of reading extremely generic Haskell code. It looks super interesting and has been done very compactly. For someone who really gets the stuff it’s probably an amazing way to communicate the thing, but for the rest of us, the jargon just forms a barrier. That’s just how specialties work, so I’m not complaining or anything. A question: > The embedding preserves limits and exponents What’s this mean? I’m especially curious about exponents because wildly different areas of math talk about exponents in ways that must be related but I don’t understand the connection.
- Twisol 6y ago
  Exponents are probably the easier aspect to understand. For instance, what is the number of distinct functions between a set X and a set Y? Well, for every input value of X, we get to choose any single output value of Y. There are |Y| choices of output, so we have |Y| * |Y| * ... * |Y|, where there are |X| factors in that multiplication. In short, there are |Y| ^ |X| functions from X to Y. So we'll often denote the function space by Y^X itself, and thus it gets called an "exponential". In the category Set, the "exponential" of two sets X and Y is exactly the set of functions from X to Y. In other categories with a concept of exponential, you get a similar internalization of collections of the category's morphisms as objects of the category. You also almost always have an exponential law, (Z^Y)^X = Z^(X*Y)). (If you interpret ^ as "if" and * as "and", you get a common law of logic that we often use when refactoring nested if-statements!) For a functor to "preserve" an exponential operation (or any other operation) is to be able to do the exponentiation either before or after the functor without changing the result. In symbols, F(X^Y) = F(X)^F(Y). (Compare with linear transformations from linear algebra, in which f(a*x + y) = a*f(x) + f(y).) Limits are a bit more fundamentally categorical, and I still don't have a good intuition for them. If you think of a functor as projecting the shadow of some index category onto your target category, a limit is in some sense a "best pre-approximation" in the target category, such that if you have a function from elsewhere in the target category into the part under your functor, you can equivalently make a pit stop at the limit object before continuing on into the functor's image. In some sense, it's like an optimal border control point just outside your functor's image -- you can systematically divert traffic through the limit without actually changing the results. I'm not sure how to intuitively interpret "preserves limits", since I guess you'd need another functor lying around whose limit is preserved under composition with your first functor. Something like F(Lim(G)) = Lim(F . G), perhaps. But now I'm just reading Wikipedia.
amw-zero 6y ago
I can’t read things like this without bringing up Leslie Lamport, the creator of TLA+. His position is that all you need for understanding computation is “regular” mathematics, i.e. set theory and predicate logic. With just this level of math, we have been able to specify, prove, and model-check sequential and distributed computations. For several decades. I was briefly interested in type theory, dependent types, etc., but have yet to have the payoff from the investment into it. Whereas investing in set theory and predicate logic has had immediate benefits to my day job. Can someone explain what type theory gets us that we don’t already have with set theory? Also, please have a read on one of Lamport’s most clear arguments on the subject: https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf https://lamport.azurewebsites.net/pubs/teaching-concurrency.....
- exdsq 6y ago
  Lamport is giving a talk at my workplace on Monday about 21st century proofs, happy to add this question to the Q&A and let you know his answer, I’m interested in this too.
- GregarianChild 6y ago
  The issue is automation: At this point (Feb 2021), the support in interactive theorem provers is just much better for type-theory based mathematics in contrast to set-theory based maths. Whether that is due to technical advantages of type-theory over set theory, or a historical accident, reflecting the much larger amount of attention on type-theory as basis for interactive provers, is a subject of much controversy. Let me cite a leading light in the formalisation of mathematics [1]: "I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two [...] I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years." Paper [2] has brought renewed attention to set-theory as a basis for automating mathematics. [1] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html https://cs.nyu.edu/pipermail/fom/2018-June/021032.html [2] https://arxiv.org/abs/1707.04757 https://arxiv.org/abs/1707.04757
carapace 6y ago
This is terrific but also frustrating: if you want people to use this stuff you've got to "bring it down the mountain". Alternately we could have a tiny elite writing crystalline mathematically perfect software and the rest of us mere mortals can just plug it together like Lego blocks. Might not be terrible?
mbrodersen 6y ago
Honest question: has anybody ever used category theory to solve a practical problem that couldn’t as easily have been solved with simple algebraic reasoning? I have so far read and understood enough category theory to get a feel for whether it is worth spending more time on or not. And my conclusion so far is: nope.

116 points by gbrown_ 6y ago

Well, that paper escalated quickly! I've dabbled in enough category theory to have some inkling of the meaning of this, but not much. I've kind of given up on expecting an epiphany from this stuff that's applicable coding in a way that significantly changes my practice in any short period of time, but I'm still tempted by the feeling that the big revelation is just a couple concepts away.

roenxi 6y ago
It seems unlikely that there will be any profound insights from category theory on how to write code, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things. Category theory is likely to contribute by giving specialists a language they can use to communicate, and it seems likely to me that at some point general tools rooted in category theory will have some sort of interesting implication for testing and debugging. Taking Haskell for example; the language isn't anything to write home about but the type checking in the tooling enabled a big improvement in writing bug free code. So there is a probably a lot on offer for the sort of people who write tooling, and less on offer for everyone else.
- pgustafs 6y ago
  “It seems unlikely that there will be any profound insights from logic on how to compute, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things.“
  - roenxi 6y ago
    It would be helpful if you fleshed that out a little, I'm curious about how you think insights from logic helps people program. I don't think I could deduce whether a developer knew or was ignorant of formal logic in a code review. Unless they give it away with a rather direct comment. Recognising that a programming language is equivalent to some mathematical construct is a very different thing from getting a practical insight about what decisions to make. My shirt is some sort of topological embedded space, but the tailoring as a field has not gained much practical insight from the study of topology. Although I would encourage any aspirations the tailors have might have to a broad education.
    - pgustafs 6y ago
      I was referring to the fact that computers themselves are the descendants of logicians — Church, Turing, von Neumann. Your argument above could have just as easily been used to attack Turing machines before the invention of the general purpose computer.
    - calhoun137 6y ago
      +1 for the request for a rephrasing. When Faraday was asked about what the practical use of his discovery of electromagnetic induction was, he famously replied, "what is the use of a newborn baby?" Which is how I read the OP
      - pgustafs 6y ago
        Here’s another great quote along the same lines: “No one has yet discovered any warlike purpose to be served by the theory of numbers or relativity, and it seems unlikely that anyone will do so for many years.” GH Hardy 1941
- GregarianChild 6y ago
  Category theorists have made this promise since the early 1990s, when the overlap between categorical methods and pure functional programming (think type theories) became clear. The really big win here was Moggi's discovery that monads neatly generalise many similar ideas in programming. (Moggi/Plotkin should have won a Goedel award for this!) This led to a great deal of activity towards generalising this to other forms of computation, in particular parallel computing (key problem: generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding). In my opinion, this has comprehensively failed to date, in the sense that (A) while you can express some parallelism in a way that can be read as a generalisation of cut-elimination / category theory, that is not surprising since (simplifying a great deal for brevity) category theory is a foundation of mathematics; but (B) when you express non purely functional computation categorically, you get extremely complicated formal systems that obscure the fundamental simplicity of what they abstract from and generally have only what they abstract from as actual model of the abstraction. Let's take Example 47 from the Native Type Theory paper: what exactly is the formal property the typing system induces? (The paper makes vague allusions to a "foreign function interface" with rho-calculus, but there is no published understanding of even the equational theory of rho-calculus. Why should I trust this paper?) What is the logic that the paper promises ("Native Type Theory gives provides a shared framework of reasoning")? What are the proof rules, so I can type them into Lean or Coq? Show me that they are better than the simple logics I get from looking at lambda-calculus operationally. Each abstraction has costs and benefits. As of 2021, the costs of categorical methods outside of pure functional languages outweigh their benefits. I worked in categorical methods for programming and changed the field, when I realised this.
  - siraben 6y ago
    > generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding How would you generalize the correspondence between cut-elimination and beta-reduction to cut-elimination and parallel composition, and what is meant by hiding here? I would be curious to know of relevant work in the area.
    - 6y ago
- specialist 6y ago
  > profound insights from category theory on how to write code Sure. But as u/feniv hinted upthread, I'm also optimistic about the impact on language design (noodling). I too have a hobby toy language. For the type system, I just want to use the best available science. Hopefully something practical, easy to explain, simple to use, with good enough ergonomics. While type theory is really important, it's just not my area of interest, and I'd like to defer to the experts.
- calhoun137 6y ago
  > It seems unlikely that there will be any profound insights from category theory on how to write code I strongly disagree with this. To me it does not seem "unlikely", quite the opposite. The reason I feel so strongly about this is that computer science is a subset of pure mathematics, its the part that deals with algorithms and computation. There are many questions in computer science which cannot be answered without an appeal to pure math (e.g., what is the best possible compression algorithm) All of computer science began as a result of the work of Hilbert on the foundations of logic[1]. This is what led to Turing's paper on Turing Machines. Since that time, mathematicians have done a lot of exciting work on foundations. Category theory has completely transformed the way we think about abstract mathematical objects; and type theory is very exciting in that it brings mathematics closer to a programming language which is compiled in the human brain and is done with pen and paper. It's seems to me very likely that in the future, code writing standards will change and get better, and will not remain the same. Towards that end, it makes sense that improvements will come from a better understanding of foundations, since that is where it all started. Curious for your thoughts? [1] https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:text=The%20system%20Hilbert%20asked%20for,than%20first%2Dorder%20Peano%20arithmetic.&text=Thus%20a%20satisfactory%20answer%20to,already%20believe%20PA%20is%20consistent https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:....
  - threatofrain 6y ago
    What has been your interest in category theory? How has category theory empowered your work?
    - calhoun137 6y ago
      My interest in category theory is just as a hobby and an amateur; but I have gone pretty deep reading lots of books and so on. To be fair, category theory has not empowered my work (in programming) at all.
      - feanaro 6y ago
        I find category theory empowers my programming in the design step, much more so than when actually writing code. It enables me to find a more elegant design from the outset and be sure of its utility and elegance even before I program it.
threatofrain 6y ago
But category theory is very foundational theory. It would similarly be like learning set theory without further goals, which would be fine if you think of it as alternative Sudoku. As a foundational language it’s there to formalize mathematical objects, but that doesn’t mean people think in either set or category theory, as opposed to higher level objects in their domain.
- acjohnson55 6y ago
  Totally agree. Just musing on my desire to fully understand this paper, but with the knowledge that all the steps to get there probably won't do much for me outside their own satisfaction. Which, admittedly, might be fun.
calhoun137 6y ago
> I've kind of given up on expecting an epiphany from this stuff that's applicable coding in a way that significantly changes my practice Same. It makes me kind of sad that pure math is not more helpful here! I think its possible that coding standards today are really high quality, and that any improvements are going to require a revolutionary paradigm shift in how we think about programming at an extreme level of generality. That's where pure math comes in, its a good place to shop around for new ideas, since we are kind of at a local maximum now in terms of best practices, imo. This is how I use math while coding: Instead of tinkering with numbers, just calculate the thing and get all the numbers right the first time. When trying to solve a problem, it's super helpful to have spent years proving theorems in pure math, it helped me compile programs in my head. When I am suuuuuuper stuck and need to figure out if what I am trying to do has already been done in math somewhere. When constructing an overall plan for a project, using abstract concepts in mathematics to properly anticipate the limits of what various implementations will be in order to pick the best one.
- tsss 6y ago
  Unfortunately, I think quality simply isn't needed for all the web shops and trivial CRUD applications that most programmers work on.
proc0 6y ago
CT helps advance Denotational Semantics, so syntax is written closer to math syntax, which I think is approaching computation in a much more stricter way and therefore leveraging the "magic" of math. Of course the price is paid in complexity of the theory and learning curve to understand it, which kills its practicality.
carapace 6y ago
Have you seen "Compiling to categories"? > 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. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages. http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/

siraben 6y ago

A good introduction to categorical logic is [0], introducing the simply-typed lambda calculus along with the categorical semantics for each construction (cartesian closed categories). The later sections include topics mentioned in this article such as hyperdoctrines, categorifying quantifiers, and dependent types. [0] https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf

3PS 6y ago
CMU also currently has a course in categorical logic [0]. Internally, the only prerequisite is a course in category theory. The course notes can be found at [1]. [0] http://mathieu.anel.free.fr/CLcourse.html http://mathieu.anel.free.fr/CLcourse.html [1] http://mathieu.anel.free.fr/mat/80514-814/Awodey-Bauer-catlog(2019).pdf http://mathieu.anel.free.fr/mat/80514-814/Awodey-Bauer-catlo...

chewxy 6y ago

I followed this until the part just slightly after "see how natural it is?" Then it's suddenly How to Draw an Owl. I don't follow the monoid part. Anyone can help elaborate?

siraben 6y ago
> Dependency is pervasive throughout mathematics. What is a monoid? It’s a set M, and then operations m,e on M, and then conditions on m,e. Most objects are constructed in layers, each of which depends on the ones before. Type theory is often regarded as “fancy” and only necessary in complex situations, similar to misperceptions of category theory; yet dependent types are everywhere. A monoid is (S,•,e): a set S equipped with a binary operation • : (S,S) -> S such that for all x, y, z in S, x•(y•z)=(x•y)•z, and an element e in S such that for all x in S, x•e=e•x=x. Examples of monoids include (String,concat,""), (int,0,+) and so on. One recurring theme in universal algebra and category theory is the notion of an algebra[0], in programmer terms it's like a module declaration. (see also F-algebra[1] which is heavily used in functional programming to formalize the notion of folding and more) Dependent type theory allows one to encode these algebras, e.g. encoding monoids and their laws in Coq's type system CoC[2]. Just like how ADTs in Haskell/OCaml and enums in Rust are comprised of a "sum of products", products and sums can be generalized in dependent types as well: Length-indexed lists via the dependent sum: Σn:ℕ.List(n) consists of dependent pairs ⟨n,l:List(n)⟩. Σn:ℕ.List(n) can be read as a function that takes a natural number n and returns a type List(n) Type-parametrized types: ΠS:Set.List(S) consists of dependent functions λS:Set.φ(S), ΠS:Set.List(S) can be read as a function that takes a type S and returns a type List(S) So to encode monoids in a dependent type theory using those dependent sums and products, we can just put the operations and laws into some big record, say Monoid:= ΣM:Set. Σm:M²→M. Σe:()→M. Π(a,b,c):M³.m(m(a,b),c)=m(a,m(b,c)). Πa:M.m(e,a)=a=m(a,e). Compare this to [2]! [0] https://en.wikipedia.org/wiki/Universal_algebra#Basic_idea https://en.wikipedia.org/wiki/Universal_algebra#Basic_idea [1] https://en.wikipedia.org/wiki/F-algebra https://en.wikipedia.org/wiki/F-algebra [2] https://gist.github.com/puffnfresh/11258181#file-monoid-v-L5 https://gist.github.com/puffnfresh/11258181#file-monoid-v-L5
- siraben 6y ago

feniv 6y ago

Seems like this is an extension of the Curry-Howard-Lambek isomorphism [1] relating type theory, logic and category theory together. I find that to be one of the most beautiful results in computer science and have been working on a practical language built on the same principles for a while (A mix of Haskell, Prolog and APL in a python-like language) [1] https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence

Tabzz98 6y ago
Is there any online material on this language?
- feniv 6y ago
  Not yet. I've specced it out, but still working on the implementation. Here's a hand-written example showing how you can specify the constraints to validate a Knight's tour. You can then enumerate over the types to get valid tours. https://gist.github.com/Feni/d819f120a7d179bc472c94df9471e600 https://gist.github.com/Feni/d819f120a7d179bc472c94df9471e60...

jimmyed 6y ago

I am a literal newbie to this field. How is this field related to logic?

guerrilla 6y ago
I suggest starting by looking up the Curry-Howard isomorphism.
blovescoffee 6y ago
How much of a literal newbie? Are you familiar with predicate logic / any formal logic? Are you familiar with any basic modern algebra like Group theory?
- jimmyed 6y ago
  I was educated in the UK, so have a good grip on the highschool math there, but not much beyond that. I did try to plough thru SICP, that's a work in progress. Too little you'd say?
  - blovescoffee 6y ago
    Well it's too little to understand immediately but you can definitely come to grasp this stuff. There are a lot of mathy words here that do warrant their invocation but don't mean that the math is arcane. You seem like you're interested which is all that matters. I'm going to be slightly handwavey/generalize here but I think it may be helpful. Predicate Logic is the basic logic that humans think of when they think "logic." It's, if-this-then-that style thinking with only basic "tools". Predicates are statements that can lead to other statements, for instance the predicate "it's raining" could imply the predicate "I will wear a jacket." You can even combine predicates such as, if "I'm hungry" _and_ "I have food in the fridge" then "I will eat." Typically, we use symbols instead of sentences so it will look more like (A and B) -> C. Assuming you've done some programming, you're already used to predicate logic in the form of if-else statements. You've also been exposed to type theory. I think SICP is in scheme so types are a little bit hidden but if you've programmed any of the modern non-lisp languages i.e. Python, Java, C, etc. then you've seen types. Types are ints, floats, strings, etc. You know how you can add two numbers but you can't add a number and a string without special rules? (1+1 == 2 but "cat" + 1 == ???) Type theory concerns these rules and a bit more. A question that type theory helps answer is, what are we permitted to do with certain classes of objects? Once the blog post gets into dependent types, I think it becomes a bit tricky to pick up. Dependent types are types that "depend" on other information. For instance, we might have a type called array which is a sequence of numbers of any length. We might further have a dependent type called the PointTripleArray := Array<3> i.e. it's an array with 3 terms and they type of PointTripleArray is the dependent type. There are other more complicated ways to use dependent typing but I'll skip those. Honestly, I kind of understand the rest of the post but not well enough to start explaining here. I wish I could. I think this is enough to get you started reading and learning though.

calhoun137 6y ago

I really like this idea! I first got into type theory as a result of an answer by Carl Mummert to a question I asked on Math StackExchange[1]. I even wrote a blog post about it a year later[2]. Ever since then, I have considered type theory to be my favorite version of the foundations of math. I have often played around in theoretical foundations theory to discover as many connections as possible between foundations of math and computer science. That being said, I think the perspectives offered by set theory and category theory are extremely valuable, and that these three approaches compliment each other, and sometimes one is better than another for a specific purpose. This is the first time I had really seen the possibility to reformulate computer science to bring it closer to mathematics. How exciting! [1] https://math.stackexchange.com/questions/1519330/is-it-possible-to-formulate-category-theory-without-set-theory https://math.stackexchange.com/questions/1519330/is-it-possi... [2] https://medium.com/@calhoun137/a-programmers-way-of-thinking-about-sets-and-categories-3f10ef2fa72c https://medium.com/@calhoun137/a-programmers-way-of-thinking...

6gvONxR4sf7o 6y ago

This whole post is above my head, reminiscent of reading extremely generic Haskell code. It looks super interesting and has been done very compactly. For someone who really gets the stuff it’s probably an amazing way to communicate the thing, but for the rest of us, the jargon just forms a barrier. That’s just how specialties work, so I’m not complaining or anything. A question: > The embedding preserves limits and exponents What’s this mean? I’m especially curious about exponents because wildly different areas of math talk about exponents in ways that must be related but I don’t understand the connection.

Twisol 6y ago
Exponents are probably the easier aspect to understand. For instance, what is the number of distinct functions between a set X and a set Y? Well, for every input value of X, we get to choose any single output value of Y. There are |Y| choices of output, so we have |Y| * |Y| * ... * |Y|, where there are |X| factors in that multiplication. In short, there are |Y| ^ |X| functions from X to Y. So we'll often denote the function space by Y^X itself, and thus it gets called an "exponential". In the category Set, the "exponential" of two sets X and Y is exactly the set of functions from X to Y. In other categories with a concept of exponential, you get a similar internalization of collections of the category's morphisms as objects of the category. You also almost always have an exponential law, (Z^Y)^X = Z^(X*Y)). (If you interpret ^ as "if" and * as "and", you get a common law of logic that we often use when refactoring nested if-statements!) For a functor to "preserve" an exponential operation (or any other operation) is to be able to do the exponentiation either before or after the functor without changing the result. In symbols, F(X^Y) = F(X)^F(Y). (Compare with linear transformations from linear algebra, in which f(a*x + y) = a*f(x) + f(y).) Limits are a bit more fundamentally categorical, and I still don't have a good intuition for them. If you think of a functor as projecting the shadow of some index category onto your target category, a limit is in some sense a "best pre-approximation" in the target category, such that if you have a function from elsewhere in the target category into the part under your functor, you can equivalently make a pit stop at the limit object before continuing on into the functor's image. In some sense, it's like an optimal border control point just outside your functor's image -- you can systematically divert traffic through the limit without actually changing the results. I'm not sure how to intuitively interpret "preserves limits", since I guess you'd need another functor lying around whose limit is preserved under composition with your first functor. Something like F(Lim(G)) = Lim(F . G), perhaps. But now I'm just reading Wikipedia.

amw-zero 6y ago

I can’t read things like this without bringing up Leslie Lamport, the creator of TLA+. His position is that all you need for understanding computation is “regular” mathematics, i.e. set theory and predicate logic. With just this level of math, we have been able to specify, prove, and model-check sequential and distributed computations. For several decades. I was briefly interested in type theory, dependent types, etc., but have yet to have the payoff from the investment into it. Whereas investing in set theory and predicate logic has had immediate benefits to my day job. Can someone explain what type theory gets us that we don’t already have with set theory? Also, please have a read on one of Lamport’s most clear arguments on the subject: https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf https://lamport.azurewebsites.net/pubs/teaching-concurrency.....

exdsq 6y ago
Lamport is giving a talk at my workplace on Monday about 21st century proofs, happy to add this question to the Q&A and let you know his answer, I’m interested in this too.
GregarianChild 6y ago
The issue is automation: At this point (Feb 2021), the support in interactive theorem provers is just much better for type-theory based mathematics in contrast to set-theory based maths. Whether that is due to technical advantages of type-theory over set theory, or a historical accident, reflecting the much larger amount of attention on type-theory as basis for interactive provers, is a subject of much controversy. Let me cite a leading light in the formalisation of mathematics [1]: "I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two [...] I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years." Paper [2] has brought renewed attention to set-theory as a basis for automating mathematics. [1] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html https://cs.nyu.edu/pipermail/fom/2018-June/021032.html [2] https://arxiv.org/abs/1707.04757 https://arxiv.org/abs/1707.04757

carapace 6y ago

This is terrific but also frustrating: if you want people to use this stuff you've got to "bring it down the mountain". Alternately we could have a tiny elite writing crystalline mathematically perfect software and the rest of us mere mortals can just plug it together like Lego blocks. Might not be terrible?

mbrodersen 6y ago

Honest question: has anybody ever used category theory to solve a practical problem that couldn’t as easily have been solved with simple algebraic reasoning? I have so far read and understood enough category theory to get a feel for whether it is worth spending more time on or not. And my conclusion so far is: nope.