[lmm]

> In OO languages (Java, C#, C++, etc...), and functional ones (F#, Haskell, OCaml, etc...) types do not validate the correctness of logic, they evaluate the correctness of data structures and their access/mutation as they are manifested in the language.

Nonsense. Types validate whatever you use them to validate, which can certainly include what we usually call "logic".

> Types have little (or nothing) to do with program correctness

On the contrary, they're still the most effective technique we've found for improving program correctness at low cost.

[bnert]

> Types validate whatever you use them to validate, which can certainly include what we usually call "logic".

I'd love an example of this! I concede that I could be wrong on the point's of ML/Haskell families, however, it relies on the practitioner correctly using the type system to the extreme (at least, that is my impression). C++ and other similar OO's, the type system isn't as compelling as a correctness measure.

> On the contrary, they're still the most effective technique we've found for improving program correctness

In which domain are you working in where this has been the case? It may be my experience, but types as I have seen them used in industry have been more as "data containers with some behaviors".

I'd appreciate some examples of where you think I may be getting types wrong or missing the point.

[lmm]

> I concede that I could be wrong on the point's of ML/Haskell families, however, it relies on the practitioner correctly using the type system to the extreme (at least, that is my impression).

I wouldn't say it's "extreme", it's very normal and natural. You just stick everything in the types and it works.

> C++ and other similar OO's, the type system isn't as compelling as a correctness measure.

Agreed that C++-style types are awful. You can generally encode whatever you need if you work hard enough at it - e.g. https://spin.atomicobject.com/2014/12/09/typed-language-tdd-... - but it's painful.

> In which domain are you working in where this has been the case? It may be my experience, but types as I have seen them used in industry have been more as "data containers with some behaviors".

> I'd appreciate some examples of where you think I may be getting types wrong or missing the point.

I've worked in "regular industry" and found types to be very effective. Let me turn it around: what kind of logic errors are you seeing that you think wouldn't be eliminated by using types? Types can't help you avoid errors in the specification itself, and there are a few domains where they may not yet be practical (mainly math-heavy things like linear algebra, where there's centuries' worth of mathematics that's applicable except where it isn't, and we just don't capture all of that in practical type systems yet), but the vast majority of the time you can construct your types in ways that force your logic to be correct because you just don't offer the ability to do the wrong thing.

[bnert]

> I wouldn't say it's "extreme", it's very normal and natural. You just stick everything in the types and it works.

Ah, then I seem to be missing the point/intention. Thanks for illuminating that it should feel "natural". I think I need to spend more time with ML/Haskell families.

> ... the vast majority of the time you can construct your types in ways that force your logic to be correct because you just don't offer the ability to do the wrong thing

I think that is where I haven't had experience, nor much exposure to, when it comes to "static typing" in the true sense/intention of making a program correct. More so (which I think I loosely alluded to), is that the type system was being used to "model objects in the real world".

> what kind of logic errors are you seeing that you think wouldn't be eliminated by using types?

Classic "logic" stuff. Forgetting to modify and return a map given some other information. Accidentally returning the inverse of a boolean (i.e. !isSomething(x) vs isSomething(x)), incorrect adds or bit shifts, concurrent access to shared data structures (shared memory may be a more apt term), reconciling two different pieces of data into a shared one, algorithmic implementations (though I think you touched on this being less likely when using a type system designed to encourage correct algorithms by applying type theory, so it may be moot).

To maybe give some clarity to what I mean by correctness, I mean does the program match the expected behavior of the programmer. In playing around with F#, I've written buggy F#, but the types all matched up. I had a guarantee that my program would run in a non-faulty manner (bar any system fault), but the program was not correct.

> and found types to be very effective

I'm very curious where you've seen this be very effective (if you're able to share), and with what language/technology.

---

Also, as a last quip, I am enjoying learning about your perspective with type systems. There are some points you have brought up which have caused me to think harder and in more depth about the concept and it's application, and want to voice that I appreciate you putting in the time to have this exchange. Want to this up before I forget, since it is getting late in my neck of the woods.

[lmm]

> Classic "logic" stuff. Forgetting to modify and return a map given some other information. Accidentally returning the inverse of a boolean (i.e. !isSomething(x) vs isSomething(x)), incorrect adds or bit shifts

If something really is just a map or a boolean or an integer then you can't avoid this kind of thing. But usually it isn't, it's something meaningful in your domain, and then you can make and enforce the right distinctions. CachedResults is not the same as FullyPopulatedResults (and neither is just a Map); rather than x and a flag for whether x isSomething, how about an Either XThatIsSomething XThatIsNotSomething? Adds and bitshifts are a wide range of operations, and if you're doing deep numerical work then that's one place where I've found that existing type systems often can't keep up, but a lot of the time you're in a domain where you don't need to do that - e.g. if you only need to add values then you can use a type that wouldn't even allow you to subtract them (indeed most of the time I see people using integers they're opaque IDs that it never makes sense to do anything mathematical with - it would be nonsense to multiply a user ID by a permission group ID, so why expose them as integers?).

> I'm very curious where you've seen this be very effective (if you're able to share), and with what language/technology.

Various industries (finance, adtech, messaging), largely "backend" whether direct API backends or more batchy/offline "big data" processing, but also even web frontends. Mostly Scala.

[theonething]

> If something really is just a map or a boolean or an integer then you can't avoid this kind of thing. But usually it isn't,

No matter how much you abstract out and dress up a boolean, at its heart it's still a boolean value and I don't see how making a custom type based on boolean would prevent returning the inverse of a boolean value bug.

[lmm]

Most of the time a "boolean" isn't a boolean - it's a flag to indicate one of two different things, which is something you can represent more directly.

[_dain_]

Are you familiar with the idea of "making illegal states unrepresentable", and "parse, don't validate"?

https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...

You brought up the examples of doing the wrong thing with booleans. With a good type system you can cut down on needing to use booleans in the first place for a lot of things. Your isSomething(x) example is a good one: presumably some code after this is implicitly relying on this predicate being true about x. If you forget to do the check, or you invert the check, then that's a bug.

But another way to do this is to encode the predicate into the type system, so the compiler makes you get it right. Concretely, supposing x is a string, and you need to check if x is a valid username before invoking username-related code on x. Then you can have a function like:

    fn as_username(x: String) -> Optional[Username]

A Username is just a type alias for a String, i.e. the runtime representation is the exact same, with no overhead. You put the parsing/validation logic inside that function. Then code expecting a username will take a value of type Username rather than String. If as_username is the only function with Username in the return type, then having a value of type Username is proof that the as_username function was already called at some point previously, and gave its blessing to the underlying string so that the Optional could be unpacked.

    match as_username(raw_string) {
    // compiler forces us to handle both cases, ie we can't forget
    // to check validity
        case Some(username: Username) {
            // code in here can assume we have a proper username
        }
        case None {
            // handle what to do otherwise
        }
    }

Sure, you have to write the as_username function correctly, there's no getting around that. But you only have to get it right once.

[bnert]

> Are you familiar with the idea of "making illegal states unrepresentable", and "parse, don't validate"?

I haven't heard of those concepts/ideas before. Thanks for linking the article to define those concepts. With your example, and the article mentioning that "parsing should take place at the boundaries" (paraphrase), I can see how types (a la ML families) can be defined and composed give internal coherence once an external input has been parsed and hence validated.

Really interesting approach which I haven't considered before!

[_dain_]

Glad I could help!

[Jach]

Agree that you can use types to express and prove logical properties via compiler; it can be a fun way to solve a problem though too much of it tends to frustrate coworkers in JavaLand. It's also not exactly "low cost"; here's an old quip I have in my quotes file:

"With Scala you feel smart having just got something to work in a beautiful way but when you look around the room to tell your clojure colleague how clever you are, you notice he left 3 hours ago and there is a post-it saying use a Map." --Daniel Worthington-Bodart

> On the contrary, they're still the most effective technique we've found for improving program correctness at low cost.

This is not borne out by research, such as there is any of any quality: https://danluu.com/empirical-pl/ The best intervention to improve correctness, if not already being done, is code review: https://twitter.com/hillelogram/status/1120495752969641986 This doesn't necessarily mean dynamic types are better, just that if static types are better, they aren't tremendously so to obviously show in studies, unlike code review benefit studies.

My own bias is in favor of dynamic types, though I think the way Common Lisp does it is a lot better than Python (plus Lisp is flexible enough in other ways to let static type enthusiasts have their cake and eat it too https://github.com/coalton-lang/coalton), and Python better than PHP, and PHP better than JS. And I prefer Java to PHP and JS. Just like not all static type systems are C, not all dynamic type systems are JS. Untyped langs like assembly or Forth are interesting but I don't have enough experience.

I don't find the argument that valuable though, since I think just focusing on dynamic vs static is one of the least interesting division points when comparing languages or practices, and may be a matter of preferred style, like baseball pitching, more than anything. If we're trading experience takes I think Clojure's immutable-by-default prevents more bugs than any statically typed language that is mutable by default; that is, default mutable or default immutable (and this goes for collections too) is a much more important property than static types or dynamic types. It's not exactly a low cost intervention though, and when you really need to optimize you'll be encouraged by the profiler to replace some things with Java native arrays and so on. I don't think changing to static types would make a quality difference (especially when things like spec exist to get many of the same or more benefits) and would also not be a low cost intervention.

Some domains also demand tools beyond type proofs. i.e. things like TLA+. I think adding static types on top of that isn't very valuable, similar to adding static types on top of immutable-by-default isn't very valuable.

Last quip to reflect on. "What's true of every bug found in the field? ... It passed the type checker. ... It passed all the tests. Okay. So now what do you do? Right? I think we're in this world I'd like to call guardrail programming. Right? It's really sad. We're like: I can make change because I have tests. Who does that? Who drives their car around banging against the guardrail saying, "Whoa! I'm glad I've got these guardrails because I'd never make it to the show on time."" --Rich Hickey (https://www.infoq.com/presentations/Simple-Made-Easy/)

[bnert]

Your point about underlying data structures is spot on, in my view.

> Last quip to reflect on. "What's true of every bug found in the field? ... It passed the type checker. ... It passed all the tests. Okay. So now what do you do? Right? I think we're in this world I'd like to call guardrail programming. Right? It's really sad. We're like: I can make change because I have tests. Who does that? Who drives their car around banging against the guardrail saying, "Whoa! I'm glad I've got these guardrails because I'd never make it to the show on time."

I've been avoiding bringing up this point/example, but this is what prompted me to start thinking more deeply about types and their tradeoffs. Great talk, IMO.

[lmm]

Quips are not a good basis for decision-making. Immutability is valuable but there is no conflict between immutability and types; you should use both. As for "bugs found in the field", having switched to Scala I pretty much don't encounter them.