Hacker News Reader

Comment by mikewarot | Hacker News Reader

I don't think the problem is with advocacy itself, but the way people always pick apart examples, leaving no effective way to tell stories anymore.

Sometimes type checking is good, other times it gets in the way. It would be interesting if there were a way to compose a program with no typing, in order to quickly get to a MVP. Once done, you could then interact with the compiler/computer in a way to fully specify intent, and result with a fully typed codebase.

Being able to loosen up typing would likely have its uses as well.

View on HN

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.

It 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.

All 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.

All programs have a global state. Forcing that state onto the stack doesn't always make things simpler.

> 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.

> 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.

This is sort of being done right now, as dynamic languages have begun to adopt gradual typing... at least Python and Julia, that I know of.

If something like [JET.jl](https://github.com/aviatesk/JET.jl) become ubiquitous in Julia, one could add a function that pointed out all the places in the code where types are not fully inferred by the compiler.

It'll never be quite the same level of safety as a static language, however.

There are plenty of languages that let you type without having to "type" out a type definition, auto types in C++, type inference in Haskell. Probably most of my Haskell code I do not need to specify types. So the technology and theory exists to make this happen.

But also, when has typing ever gotten in the way? Actually having to think about the problem and the correctness of your program? It's somewhat amazing that correctness is so easily discarded. People just get stuck in a local minimum.

They don't get in the way in that regard. There are solutions they simply cannot express and sometimes the best solution is one of these.

Correctness has little to do with it. Most type systems cannot express the actually important stuff, so you need to write defensive code anyway and make sure it works.

When you write in a dynamically typed language you are going to miss static typing sometimes and vice versa. The big advantage of static typing is performance and not necessarily correctness.

I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I am not able to think of such a thing of the top of my head.

I disagree that performance is a big advantage. Perhaps there are certain optimisations that can be done if you have added more constraints? But that seems like an added benefit. I feel like there are a plethora of examples of type errors however. Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system. Seems like that rules out a whole class of possible errors with parsing input.

> I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language.

I meant to say that some of many solutions can better, typically simpler, while being just as correct because you don't need to express it in static types.

> Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system.

That is orthogonal to a type system though. If you take care of the invariants of a data-structure you are almost always going to need more than what most type systems can express.

In fact I would argue that type systems provide immediate documentation of very basic properties, which is often an advantage, but from my experience the errors it covers for you are rare, yet can be severe and confusing.

Again, having used both I'm not entirely happy with either. I prefer when static, or more generally developer-time-checks are opt-in and expressive, which seems to be a growing trend.

Statically typed languages always have escape hatches, so in that way there really is nothing that can’t be done in such a language vs a dynamic one (at least in theory)

Agreed! To clear it up: I meant the expressivity of the type system, not the language as a whole.

Note that there are downsides to type inference. Most notably, with too much type inference you quickly run into undecidability. Specifically, programs for which the question "is this well typed" is not decidable. (Essentially it allows encoding of paradoxes in the type system).

This is why Haskell and C++ do sometimes require types to be mentioned.

I mean I am not sure that is a downside, just a limitation. Sometimes yes you have to specify if there is an ambiguity. I guess usually on input, but then that is not a huge price to pay.

> other times it gets in the way

No, not really.

> Once done, you could then interact with the compiler/computer in a way to fully specify intent

Doesn't work that way. Once you went down the path of laziness and started to e.g., dumping data structures into untyped dictionaries or lists instead of properly specifying them, there is no going back without throwing out all the code and rewriting.

I come from the strongly typed world of Pascal... I wasn't thinking about dictionaries, but rather the decision to use a Byte, U32, U64, Real, Single, Double, etc. You could always use the longer, more expensive option for prototyping, then slim it down once you have a better idea of what's needed.

Similar to the way the precision of calculations in neural networks is shaved down for performance, but only as long as the output stays reasonable.

Groovy maybe?

Reply on news.ycombinator.com