5 ms·

Stuff like this is why I don't like type systems. What you want to do is easy, but it becomes difficult to explain in a sane way (15 months difficult), because

Stuff like this is why I don't like type systems. What you want to do is easy, but it becomes difficult to explain in a sane way (15 months difficult), because you need to work around the limitations of type systems. When you say "set-theoretic types", I hear, "get rid of types, just give me logic".

ryanschaefer 2y ago
> what you want to do is easy Easy to implement, hard to get correct. It inverts where you do work in a system. It can be hard to implement robust types but once that’s done it’s easy to know what you are writing is correct.
josevalim 2y ago
The work to develop the base theory, which this article presents, takes 15 months, but it doesn't take 15 months to read it (and hopefully it won't take as long to use it either). Whenever you use a programming language, you may work with data structures that took months to formalize and several more years to optimize, yet no one is saying "throw our data structures away". Even things like pretty printing and formatting a float have collectively several years of research behind them, yet the API is often a single function call. Of course, you can still not like types, and making it harder to evolve libraries over time is a good reason. But using the time it takes to formalize its underlying concepts is not a strong argument against them. The goal is that someone will spend this time, precisely so you don't have to. :)
- Conscat 2y ago
  I have seen multiple users of one certain popular programming language claim that data structures besides a dynamic length array and a hash table have no useful application.
  - caspper69 2y ago
    They wouldn't also happen to throw out memory safety guarantees one level up by using a ton of array indexing, would they?
  - tadfisher 2y ago
    Clojure? Sounds like something Hickey would say.
- practal 2y ago
  Oh, I like formalising things, don't get me wrong, and I don't mind spending time on it at all. I just don't like doing it via types, and looking at how much time you spent on what, I rest my case.
ddellacosta 2y ago
> because you need to work around the limitations of type systems. What limitations of type systems are you talking about? > When you say "set-theoretic types", I hear, "get rid of types, just give me logic". A type theory/type system is a logic, so I don't really understand this point. https://en.wikipedia.org/wiki/Type_theory#Logic https://en.wikipedia.org/wiki/Type_theory#Logic
- practal 2y ago
  Yes, a type theory is a logic, but not a particularly good one. It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice. The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage.
  - ddellacosta 2y ago
    > Yes, a type theory is a logic, but not a particularly good one. Given the context of the original post, type theory at least has the benefit of actually existing in industrial languages in the form of a bunch of implemented and in-use type systems. > It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice. > > The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage. That's helpful in understanding where you're coming from, but now I'm even more perplexed--what you've linked to seems extremely theoretical. The closest to something my industrial programmer brain can grasp and read that I'd care about (in the context of the original post we're discussing) is https://obua.com/publications/automating-abstraction-logic/1/ https://obua.com/publications/automating-abstraction-logic/1..., which seems focused on theorem proving. None of this is meant to suggest that I don't see the value in what you've linked to--it will take me some time to absorb, but I will take a closer look--but if you want to come into a discussion about a post like this one and criticize it, and more generally type systems, I think you'd be better off showing more directly how your approach can solve the same problem (or how it doesn't need to solve it, which it sounds like you're implying) in a way that doesn't take reading through a bunch of fairly abstract posts and papers or watching a five-part video series first. And if there's no actual implementation (that I can see at least) then don't expect me, an industrial programmer--like most folks on HN I would guess vs. e.g. lambda-the-ultimate or whatever--to consider it worthwhile past idle curiosity. I see value in Valim's post because it identifies a problem with type systems that I understand and have encountered, and provides an incremental and pragmatic solution to that. It doesn't seem like you're offering a coherent, practical alternative, regardless of the validity of your arguments ("It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe" makes intuitive sense to me in this context, at least).

ryanschaefer 2y ago

> what you want to do is easy Easy to implement, hard to get correct. It inverts where you do work in a system. It can be hard to implement robust types but once that’s done it’s easy to know what you are writing is correct.

josevalim 2y ago

The work to develop the base theory, which this article presents, takes 15 months, but it doesn't take 15 months to read it (and hopefully it won't take as long to use it either). Whenever you use a programming language, you may work with data structures that took months to formalize and several more years to optimize, yet no one is saying "throw our data structures away". Even things like pretty printing and formatting a float have collectively several years of research behind them, yet the API is often a single function call. Of course, you can still not like types, and making it harder to evolve libraries over time is a good reason. But using the time it takes to formalize its underlying concepts is not a strong argument against them. The goal is that someone will spend this time, precisely so you don't have to. :)

Conscat 2y ago
I have seen multiple users of one certain popular programming language claim that data structures besides a dynamic length array and a hash table have no useful application.
- caspper69 2y ago
  They wouldn't also happen to throw out memory safety guarantees one level up by using a ton of array indexing, would they?
- tadfisher 2y ago
  Clojure? Sounds like something Hickey would say.
practal 2y ago
Oh, I like formalising things, don't get me wrong, and I don't mind spending time on it at all. I just don't like doing it via types, and looking at how much time you spent on what, I rest my case.

ddellacosta 2y ago

> because you need to work around the limitations of type systems. What limitations of type systems are you talking about? > When you say "set-theoretic types", I hear, "get rid of types, just give me logic". A type theory/type system is a logic, so I don't really understand this point. https://en.wikipedia.org/wiki/Type_theory#Logic https://en.wikipedia.org/wiki/Type_theory#Logic

practal 2y ago
Yes, a type theory is a logic, but not a particularly good one. It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice. The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage.
- ddellacosta 2y ago
  > Yes, a type theory is a logic, but not a particularly good one. Given the context of the original post, type theory at least has the benefit of actually existing in industrial languages in the form of a bunch of implemented and in-use type systems. > It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice. > > The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage. That's helpful in understanding where you're coming from, but now I'm even more perplexed--what you've linked to seems extremely theoretical. The closest to something my industrial programmer brain can grasp and read that I'd care about (in the context of the original post we're discussing) is https://obua.com/publications/automating-abstraction-logic/1/ https://obua.com/publications/automating-abstraction-logic/1..., which seems focused on theorem proving. None of this is meant to suggest that I don't see the value in what you've linked to--it will take me some time to absorb, but I will take a closer look--but if you want to come into a discussion about a post like this one and criticize it, and more generally type systems, I think you'd be better off showing more directly how your approach can solve the same problem (or how it doesn't need to solve it, which it sounds like you're implying) in a way that doesn't take reading through a bunch of fairly abstract posts and papers or watching a five-part video series first. And if there's no actual implementation (that I can see at least) then don't expect me, an industrial programmer--like most folks on HN I would guess vs. e.g. lambda-the-ultimate or whatever--to consider it worthwhile past idle curiosity. I see value in Valim's post because it identifies a problem with type systems that I understand and have encountered, and provides an incremental and pragmatic solution to that. It doesn't seem like you're offering a coherent, practical alternative, regardless of the validity of your arguments ("It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe" makes intuitive sense to me in this context, at least).