3 ms·
In moving from the untyped lambda calculus to the simply typed lambda calculus, one loses the ability to have non-halting programs. For me this just illustrates
by BlackFly 5y ago
In moving from the untyped lambda calculus to the simply typed lambda calculus, one loses the ability to have non-halting programs. For me this just illustrates a fundamental point of type systems: limit the possibilities to make them understandable. Clearly I cannot describe a typical server with the simply typed lambda calculus, I need some kind of `while true: do()`.
With dynamic typing, it is easy to make programs that work with types that are extremely difficult to describe and comprehend. I think that is what TypeScript has added so much advanced type theory level functionality: it is necessary to describe what people did with dynamically typed javascript. I imagine MyPy and company will have a similar trajectory for python. People did some really incredible things in these dynamic languages, things which are very difficult to describe formally.
Meanwhile, it seems to me at least part of the point of some statically typed languages is to force people to work with simpler type systems to solve their problems. Because those simpler types may be easier to understand even if they require more effort or more code to solve the same problem. I do think Go was far too adamant for far too long about not needing generics (also known as parametric polymorphism); seems sober minds clearly disagree about where to put the boundaries. To me it seems that statically typed languages embrace the notion of "Good enough, but not perfect." They provide enough expression to solve problems, but not enough expression to describe all solutions.
- xupybd 5y agoIt seems to me that limiting possibilities is the best way to reduce complexity. Immutability, strong types, no goto, no global state and the list goes on. These all avoid the complexity of too many possibilities.
- dgb23 5y agoAll of those limitations can add complexity, specifically when they are not a good fit and you need to either work around them or break their rules. There are plenty of examples where immutability is not the right fit (or even possible) or when static types are not helpful but just increase verbosity (and complexity). They might be good defaults (especially immutability if you can afford it) but not strictly the best way to reduce complexity in every circumstance.
- mikewarot 5y agoAll programs have a global state. Forcing that state onto the stack doesn't always make things simpler.
- cheph 5y ago> I do think Go was far too adamant for far too long about not needing generics (also known as parametric polymorphism); seems sober minds clearly disagree about where to put the boundaries. Adamant is rather generous. Golang maintainers are overly defensive about serious deficiencies in an otherwise mediocre programming language. It is the worst tool for the job in almost any situation. At the moment it is easier to write correct software in Python than it is to do it in Golang and in almost all cases correctness is more important than performance.
- rocqua 5y ago> Golang maintainers are overly defensive about serious deficiencies in an otherwise mediocre programming language. It seems to me like a sentence like this is exactly what the article was arguing against.