5 ms·

Why is it worth spending time on type theory? (2013)

• deleted 1y ago
  [deleted]
• ttoinou 1y ago
  OT but is this kind of well researched user content be disappearing with AI content filling the web ? Will some places / forums keep power users interested in spending time researching and answering ? When what they produce will be ingested in future models and not sourced back to them
  • HappyPanacea 1y ago
    I'm a very small time MSE user but indeed such concerns made me reluctant to answer recently or even participate in general. The CC BY-SA requires both Attribution and ShareAlike which doesn't happen. I expect people will move to private silos of information as much as possible.
    • ttoinou 1y ago
      Yeah but how do you make sure no robots subscribe to the private silos ? Also, there's always some kind of minimal size required for spaces to be interesting for people to participate. And networks effects.
      • HappyPanacea 1y ago
        Legal means mostly and yeah indeed networks effects are the biggest obstacle.
  • deleted 1y ago
    [deleted]
• fellowniusmonk 1y ago
  As a mereological nihilist I like type theory but I wish it was type and schema theory. Treating complex types, structure, arrangement, entanglement, etc. as if it has the same realness or priority as primitive types is a mistake. It's like acting like recursion is physically real (it's not) when it smuggles in the call stack.
  • nyrikki 1y ago
    Topos theory can be added to type theory to provide a categorical semantics. But even with Grothendieck topology (total and co-total categories) requires sets with least upper bound (join) and a greatest lower bound (meet). The problem is that you get semi-algorthms, thus will only halt if true. IMHO it is better to think of recursion as enabling realizability, and forcing fixed points. The ycombinator can be used for recursion because it is a fixed point combinator. From descriptive complexity FO+LFP=SO+Krom=P, while FO by itself is AC^0 IIRC? Using model logic+relations is another path. The problem I have found is those paths tend to require someone to at least entertain intuitionistic concepts and that is a huge barrier. Mostly people tend to use type theory to convert symantic properties to trivial symantic properties for convenience. Blackburn/Rijke/Venema's “Modal Logic” is the most CS friendly book for that if you want to try.
    • layer8 1y ago
      “Semantic”?
      • nyrikki 1y ago
        Funny I fought for a good 5 min trying to convert everything to semantic on my phone, and finally gave up, figuring it also proved I wasn't a bot :) I have fixed it now. But yes: semantic, run-time, extensional, etc... from Rice/Godel/etc...
    • fellowniusmonk 1y ago
      Yes, it's interesting to see when coders start dealing with physical world problems and sensor systems and don't realize they are relying on constructivity to do anything at all. I've mostly only met other devs who have also worked in the CRDT space that grok intuitionistic reasoning.
• doppelgunner 1y ago
  Because once you understand type theory, you unlock the ability to win arguments on the internet using words like "monoid" and "dependent elimination". Also, it's comforting to know that while your life may lack structure, your types never will.
  • derriz 1y ago
    I know this is supposed to be a joke but I don’t get it? Type theory isn’t particularly heavy in terms of jargon compared to other foundational theories like category theory or set theory. These are highly technical fields of study so of course they’re going to need specific language. It would like complaining about a doctor using “fancy terms” when discussing complex medical procedures. To give a non-cynical answer: a good reason to look at type theory - if you’ve been exposed to computer science - is that it treats syntax and syntactical manipulation as foundational and can be viewed as the branch of mathematics that ties syntax and with the notion of computation.
    • JadeNB 1y ago
      > Type theory isn’t particularly heavy in terms of jargon compared to other foundational theories like category theory or set theory. And anyone who thinks their own area doesn't have jargon has just forgotten how to recognize it.
      • bevr1337 1y ago
        And quartz, of course. https://xkcd.com/2501/ https://xkcd.com/2501/
    • Twey 1y ago
      And ‘monoid’ isn't even from type theory!
    • theflyinghorse 1y ago
      Not heavy on jargon? Compared to what? It’s all jargon
• AnimalMuppet 1y ago
  Let's say I ask, "Why is it worth spending time in Baltimore?" I could get answers about the national anthem, about Camden Yards, about good restaurants and bars. Those are "tourist" answers. Or I could get answers about job availability and cost of housing. Those are "move there" answers. It seems to me that this article (if you can call it that) gives mostly "tourist" answers, not "move there" answers. Well, that's all right in a way - for an academic topic, you probably have to get tourists before you get people moving there. But the problem is that mathematicians have a large number of areas that they could visit as tourists, and nothing here tells them why type theory is better to visit than, say, algebraic topology. And that doesn't solve the original complaint. Why are so few people working in type theory? Because more of the action is in set theory and category theory, and type theory offers too little that the others don't, so nobody's going to switch. I mean, most mathematicians aren't really in foundations anyway. They're in differential equations or prime numbers or complex analysis or algebraic topology or something like that, and making your foundation type theory instead of set theory makes no difference whatsoever to those people. Only the people working on foundations care, and as I said, most of those people already work in set theory or category theory, and type theory doesn't give them a good enough reason to uproot and move.
  • derriz 1y ago
    I’m not sure Set theory and Type theory compete for the same foundations people. Type theory’s stomping ground is in the foundations of computation. I’m guessing if you sampled a theoretical comp. sci. audience, I’m pretty sure type theory would “win” the popularity contest. Somewhat similar to intuitionism and constructivism - interesting to people interested in computability but considered almost silly or at least niche by “mainstream” math theoreticians.
    • AnimalMuppet 1y ago
      Fair enough, though TFA seemed to be focused on the "foundations of mathematics" angle. If you want to say it's good for foundations of CS... I can probably agree (though the category theory folks may want a word).
    • 1y ago
• lovich 1y ago
  Where does one even start learning type theory or category theory? I’ve had a passing interest from listening in on conversation between Rust friends, but never found a place to do a like type theory 101 for software engineers
  • JonChesterfield 1y ago
    I watched these https://www.youtube.com/@hottlectures5237 https://www.youtube.com/@hottlectures5237, at least up to the point where they seemed to be diverging from things I could see application in. There's an associated book which is fairly tough going but enlightening (easier after watching some of the videos).
  • louthy 1y ago
    Bartosz Milewski’s Category Theory for Programmers lectures [1] are good. Especially paired with his book [2]. I actually find that category theory is remarkably simple. At least at the level where it applies to day-to-day programming concepts. The one major benefit I got from it, was that it helped me reason about high level/abstract structure better (which helps my architectural designs/thinking). [1] https://youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&feature=shared https://youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa... [2] https://github.com/hmemcpy/milewski-ctfp-pdf https://github.com/hmemcpy/milewski-ctfp-pdf
  • codeismath 1y ago
    Books. Some books on my shelf covering these topics: "Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search) First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof "Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo "Type-Driven Development with Idris" by Edwin Brady "Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski "Types and Programming Languages" by Pierce "Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory) "The Little Typer" by Friedman and Christiansen "Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.) For Category Theory: "The Joy of Abstraction" (2023) by Euginia Cheng "Basic Category Theory for Computer Scientists" by Benjamin C. Pierce "Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel "Categories for the Working Philosopher" by Landry
• joe_the_user 1y ago
  The OP goes on to immediate ask whether category theory or type theory can serve as a foundation for mathematics (they give a link to an article that talks of "foundational styles" but which doesn't give a process of explicitly "cutting the cord" from set theory). I think the answer by (perhaps infamous) Paul Taylor in this mathoverflow post[1] is a clearer expression of the positions of those who want to jettison traditional set theory as the foundation of mathematics. "The crucial issue is whether you are taken in by the Great Set-Theoretic Swindle that mathematics depends on collections (completed infinities)" Yes, it's important to remember that everything labeled "infinity" in math doesn't "exist-exist" but rather is some combination of unending process and arbitrary labeling (see Skolem's paradox etc). But that doesn't mean such nominally completed infinities aren't useful or even necessary for a human being to grasp mathematics. Anyway, for this debate it's worth reading all of Taylor's comment (which isn't to say I share his position but it's good to understand where the "finitests" are coming from). [1] https://mathoverflow.net/questions/8731/categorical-foundations-without-set-theory https://mathoverflow.net/questions/8731/categorical-foundati...
  • deleted 1y ago
    [deleted]
  • layer8 1y ago
    I don’t quite buy this, because we want to abstract over the stuff reachable by a particular generic process, say, over the natural numbers. We want to say, in mathematical language (i.e. as formulas), things like “whatever x we can reach in this kind of process, property P will hold for it”. This requires abstracting over all possible x, and in that abstraction, “all possible x” becomes itself an object. And we call those kinds of objects sets.
• auggierose 1y ago
  It is not worth spending time on type theory. It is quite meaningless, literally.
• js8 1y ago
  I think the answer is yes. Modern efforts to formalize mathematics use type theory a lot, specifically calculus of inductive constructions, rather than ZFC. At around 2000, I studied applied mathematics. I was curious about automated theorem proving, but I didn't understand the language (being, as most mathematicians, trained in proving with classical logic rather than type theory). Years later I discovered Haskell, which became a "gateway drug" to type theory. I wish something like Lean had existed 25 years ago, when I was a student. I think fully formal methods in mathematics are the future, and every math student should learn a bit of Lean (or a similar tool, but IMHO Lean has the best tutorials, aimed at people with traditional education). Hence, everybody should learn basics of type theory.
• labrador 1y ago
  I'm just an old country imperative programmer, not a big city functional programmer, so excuse my ignorance, but I had an ephiphany the other day. Functional programmers with strict types organize their data with complex types, while I do the same with classes. I need to do more research to verify this, but it explains the focus on types in functional languages to me.
  • js8 1y ago
    One of the core concepts in type theory is the function type. It's a kind of building block. So perhaps better would be to say functional programmers organize everything using functions. I suggest you look at simply typed lambda calculus, it gives a basic rationalization of types in functional programming.
  • Twey 1y ago
    Typically when an OOP programmer says the word ‘class’ they mean one (or both) of two things, depending on their favourite OOP language: - a factory for objects, that hides some internal state of the object; - a static construct that gives a name to some (‘public’) subset of the behaviour of those objects, and which a type-checker can then use to ensure that the use of the objects adheres to the intended contract. They're both mechanisms for encapsulation of internal behaviour (that may change at any time) while providing a blessed public API that you promise will stay the same (or at least only change in certain ways, under a strict discipline like semver or ‘we'll tell you on the mailing list’). The difference is that the former is runtime (dynamic) behaviour, while the latter is compile-time (static) behaviour. The former maps to functions (or, with state, closures), not types, in functional languages (see ‘objects are a poor man's closures, and vice versa’ [1]), and the latter… is types :) The same typing concept that ensures correct interaction with objects can also be used to ensure correct interaction with functions or other data types, though since functional languages are easier to type than OO languages strictly-typed functional languages tend to have stronger type systems that capture more properties, like effects. [1]: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/msg03277.html https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/... From one perspective, there's a spectrum imperative <-> procedural <-> OOP <-> functional that is about how tightly scoped state changes are. In that view, functional languages are just the natural next step: if the whole point of OOP is to scope state, a functional language is just an OOP language with _even more_ tightly scoped state. The philosophy (uncontrolled state changes are scary and hard to reason about: add language constructs that allow the reader to see at a glance how far they have to look for the knock-on effects of a given state changes) is the same, just the implementation is different.