> It was to provide a small, parsimonious foundation for all of mathematics with a minimal number of "obvious" commitments, to give us confidence that the mathematics we're doing is consistent
I would argue that type theory does a better job at this than set theory. With set theory, you need to believe in two separate things: (1) the language of first-order logic (or some other logic) with its inference rules, (2) the set theory axioms. With type theory, there is only the language of lambda terms. And the rules for type theory are straightforward and intuitive for programmers, e.g., you can only call a function on an argument if the function's domain matches the type of the argument. Contrast that with set theory, where you have highly counterintuitive and seemingly arbitrary axioms like the axiom of separation.
> I do not understand why homotopy type theory posts are so popular on this website.
Martin-Löf type theory (and, therefore, homotopy type theory) is like an idealized programming language that is capable of expressing both programs and proofs, such that you can prove your code correct in the same language. Hacker News is a mostly technical community that often likes to geek out on programming languages.
Homotopy type theory is an especially cool flavor of type theory that finally gives a satisfying answer to the question of when two types should be considered propositionally equal.
For people who know Rust, Haskell's type classes are like a more general version of Rust's traits. But that comparison suggests the wrong chronology; Haskell's type classes came a couple decades earlier.
It's not about biases. Using immutability is not just some personal preference. It's common knowledge that mutability everywhere is a bad practice. That's why there's a trend toward immutability by default in newer languages.
> Thankfully, this sort of analysis tends to use "constructive logic"; in which case, we're told why some property isn't provable (either because we're given a counterexample proving it's incorrect, or we're told which assumptions/preconditions need to be proved first)
> The net effect of this would be that I type "mutable" all over the place
You might want to consider adopting a more modern programming style for the benefit of your coworkers (and possibly yourself). Mutability all over the place is a nightmare, speaking as someone who currently has to work in a large codebase written like that. It's hard to predict what value a variable is going to have at any particular point in your code, since instead of only having to check where the variable is defined, you have to audit all the code between the definition and the use. For the same reason, it's hard to guarantee that your invariants are maintained, since there is a much larger surface area to check.
What's wrong with this? I need a way to describe techniques that make it easier to...well I don't even know another way to say it. Maybe I'm biased by my experience in formal verification, a field in which it's expected that you can formally study a program's behavior.
I think there might be a loose connection. When you want to prove something using mathematical induction, you must come up with an "induction hypothesis". This requires cleverness which could possibly be described as the product of inductive reasoning (in the philosophical sense). Essentially it amounts to finding a general principle that can be specialized to prove each of the inductive steps.
The main difference to me is that, with inductive reasoning (in the philosophical sense), you converge on a general principle but it might be wrong—it is only probable. Mathematical induction is the tool needed to close the gap—to turn a hypothesis which could be wrong into a bulletproof mathematical theorem. Of course, if your induction hypothesis didn't turn out to be right, you won't be able to complete the proof.
I use the Coq theorem prover to write induction proofs all the time, and often you have to try out different induction hypotheses until you get one that finally works. The process my brain goes through to come up with these induction hypotheses feels like "inductive reasoning" in the philosophical sense as I understand it.
> I wish that all language design went through a filter where every character mattered like the designer was in an episode of Squid Game.
Yes, I totally support this! Coming from languages like Haskell, most languages look so unnecessarily noisy to me. Cut the fat!
> Anyone who proposes a way to minimize Lisp parentheses, who hasn't introduced a symbol for missing outline levels, is just pulling out chunks and hasn't used their system to write thousands of lines of code.
What are outline levels? I tried Googling it but didn't find anything.
> C syntax is ground glass in my eyes.
Is that a good thing? I'm not sure what you mean by it.
As someone with years of experience writing machine-checked proofs in Coq, I cannot imagine the term "Software Engineer" shifting to that meaning, even though it may make sense when compared to other engineering disciplines. The programmers who have no experience with this technology outnumber us many thousands to one. They'd never sign off on it.
That said, I'm all for anything that results in more appreciation for mathematical rigor in programming. It's like puling teeth trying to get colleagues to use tools/languages that help with reasoning about code (even just a good type system), and for a lot of programmers math seems to be an unapproachable alien language.
One thing I'd like to change about the software industry is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program. The misconception there is that the all of the program's behavior needs to be specified in order for formal verification to be useful. Why can't gradual formal verification be a thing?
> You might say "but it will make it more confusing for people who already know the FP terms"
People who already know FP would be fine. Newcomers would be the ones to suffer. We already have a large number of tutorials, blogs, books, etc. using the existing terminology. For a programmer new to FP to tap into that they would need to learn both the "friendlier" (whatever that means) terms as well as how they map to the math terms.
We need to stop treating math like some unlearnable alien language—you'd still need to learn it anyway, regardless of what you call the abstractions. Also in many (perhaps most) cases there is no clear choice for the "friendly" term. Words like "chainable" would be highly ambiguous, as many different types of abstractions support some notion of "chaining". This would likely result in bikeshedding and more divergence in terminology and less precision in meaning.
If you think the math terms are bad, try asking a mathematician to rename the terms in their field. They'll tell you the same thing.
I agree about the math terminology, but I think it would be more confusing if we created a completely different set of vocabulary for the same concepts. So I don't really know what to do: refer to something by its proper name, or create a new, less precise name to make it sound less scary? Why do we find certain identifiers scary in the first place?
> The lambda calculus is an entirely arbitrary way to organize things in math. It’s not based on nature or truth at all.
Lambda calculus, category theory, and logic are essentially 3 sides of the same coin (the Curry-Howard-Lambek correspondence). The rules of lambda calculus match those of natural deduction. It runs quite a bit deeper than you're suggesting here. It's not just some arbitrary formalism.
I wonder why they don't just use the highest precision possible given whatever representation of numbers they're using? I know these extra digits would be unlikely to ever matter in practice, but why even bother truncating more than necessary by the hardware? (Or do they not use hardware to do arithmetic calculations?)
Categories are objects and morphisms with identities and composition, subject to some coherence laws characterizing identities and stating the associativity of composition. Category theory studies categories and related constructions, such as functors, natural transformations, adjunctions, (co)limits, universal properties, etc.
> And yes it has everything to do with AI
No, category theory is not about AI. My training was certainly sufficient for me to refute that connection, and the way you keep referring to my "training" rubs me the wrong way.
This article is completely incongruous and reveals fundamental misunderstandings of category theory. That's actually being generous; most of the content isn't even coherent enough to be wrong.
> Category Theory (at least applied to computing) studies how instructions are assembled into running programs.
Um, no? As a software engineer who has studied category theory, I use it mostly for denotational reasoning about programs, and to inform type-level decisions. It has nothing to do with "instructions". Perhaps a generous interpretation of this statement would be that monads, one very specific concept in category theory, can be used to model imperative programs—but that would be highly reductionist.
> That’s not to say that FP is useless. FP is obviously quite useful in many situations - but perhaps not be enough to displace the central role of wrapper functions / lambda calculus.
What? Functional programming _is_ lambda calculus. The idea of it displacing lambda calculus makes no sense.
> Why? Mathematically speaking, Category Theory is basically the same as Relational Theory (at least applied to Sets).
Oof. Rel is one category; Set is another.
> There is this fanciful notion of a “computational trinity”- the idea is that devs can somehow write to a single source of “truth” and let artificial intelligence / automation decide how it gets translated to hardware.
No, the trinity refers to the connections between category theory, logic, and programming. It has nothing to do with AI.