[tsss]

> type systems are totally unable to express algorithms

You don't know much about types if you think that.

As for dynamic typing "helping" you to find code that you need to write tests for: There are already far more sophisticated static analysis tools to measure code coverage.

[blacktriangle]

  doubler :: Num a => [a] -> [a]
  doubler xs = take 2 xs

Passes the type checker, thanks type system! /s

I like static typing, but static typing advocates seriously overstate how much protection the type system gives you. Hickey really said it best: "We used to say 'If it compiles it works' and that's as true now as it was then."

As for dynamic typing "helping find code to write tests", that's not a feature, it's a huge downside. Neither side is perfect, but in my experience the benefits of the static checker are overblown since I need to write tests anyways. And also like you say, there's a variety of great static analysis tools you should be using as well.

[hota_mazi]

Proving that your program is consistent is only one of the many benefits that a static type system brings you.

I'd say the main one is that it enables automatic refactorings, which are mathematically impossible to achieve when you don't have type annotations.

Thanks to automatic refactorings, code bases are easier to maintain and evolve, as opposed to dynamically typed languages where developers are often afraid to refactor, and usually end up letting the code rot.

It's also a great way to document your code so that new hires can easily jump on board. It enables great IDE support, and very often, unlocks performance that dynamically typed languages can never match.

[capableweb]

> I'd say the main one is that it enables automatic refactorings, which are mathematically impossible to achieve when you don't have type annotations.

Yeah, it's really not impossible. Maybe in theory, it's "mathematically impossible", but in practice, doing a search on your local codebase and understanding the code you find makes it easy to do refactors too. Dynamic languages also can help making refactoring obsolete, as you can create data structures that doesn't matter if they are User or Person, as long as it has a Name, print the name (or whatever, just a simple example) whereas with a static type system, you'd have to change all the User to Person. You're basically locking your program together, making it coupled and harder to change.

> It enables great IDE support

Is there anything specific that IDEs support for static typing that you can't have for dynamic languages? I mostly work with Clojure and have everything my peers have when using TypeScript or any other typed language.

> unlocks performance that dynamically typed languages can never match

I think there is a lot more to performance than just types. Now the TechEmpower benchmarks aren't perfect, but a JS framework is at the 2nd place in the composite benchmark, beating every Rust benchmark. How do you explain this if we consider your argument that types will for sure make everything faster and more efficient?

https://www.techempower.com/benchmarks/#section=data-r20&hw=...

[pdimitar]

I'm not sure when did this become about typing systems promising you'll never write tests? IMO nobody says that.

Let me give you one example.

When I'm coding in Rust and I forget to match on one of my sum type's variants, the compiler will immediately yell at me.

When I'm coding in Elixir, the compiler doesn't care if I do exhaustive pattern matching because it doesn't know all possible return values. In these conditions it's extremely easy to not write code that deals with a return value that appears rarely.

That's one of the values of static typing for me.

[blacktriangle]

That was meant as a response to tsss apparently overvaluing his type checks.

The pattern matching example is one that often comes up talking about typing. Yes it's great that the type checker finds all the places you didn't deal with your new sum type varient...except here's the rub. All that code was working just fine before. Your static type checker is forcing a bunch of code that never needed to know or care about certain values onto all places where you used pattern matching. I don't think this speaks to the value of static typing, I think it suggests that pattern matching is a bad idea that leads to overly coupled code where parts of the system that really shouldn't need to know about each other are now forced to deal with situations they don't care about.

[pdimitar]

> Your static type checker is forcing a bunch of code that never needed to know or care about certain values onto all places where you used pattern matching.

It's not "forcing" anything, you are evolving your program and the compiler is helping you not play a whack-a-mole by actually telling you every place that must be corrected in order to account for the change.

Wasn't aware that evolving a project is called forcing. :P

> I think it suggests that pattern matching is a bad idea that leads to overly coupled code where parts of the system that really shouldn't need to know about each other are now forced to deal with situations they don't care about.

That's a super random statement, dude. If a sum type change makes 7 places in your code not compile then obviously those pieces of code do care about it -- you wouldn't write it that way if it didn't. Nobody put a gun on your head forcing you to include the sum type in these places in the code just because, right?

Overall I am not following your train of thought. You seem to be negatively biased. I've seen from my practice only benefits by enforcing exhaustive pattern matching. Many times I facepalmed after I got a compiler error in Rust and was saying "gods, I absolutely would've missed that if I wrote it in a dynamic language".

[tsss]

You can very easily write a "safe" version of that function that will not type check and in this case you don't even need dependent types. So: bad example on your part.

[blacktriangle]

So you're saying without dependent types you can express in a type a function that will return double each element in the list thus removing the need to test the function?

If you can do that, that's awesome, but I'm not seeing how.

[tsss]

I meant that you can write a version of your function with the same definition that will not type check since `take 2` is illegal for lists of length less than 2.

As for a function that will "double" a list, i.e. turn [1,2] into [1,1,2,2]: That is definitely possible with dependent types as they can express arbitrary statements. I'm not sure if you can do it without dependent types, but I'm inclined to say yes: something like an HList should work. Universal quantification over the HList parameters will ensure that the only way to create new values of the parameter types is to copy the old ones, as long as you disallow any form of `forall a. () -> a` in the type system.

Something like this, which is just the `double` function lifted into the universe of types, _might_ work, though its utility is questionable:

    type family DoubleList xs :: 'HList -> 'HList where
        DoubleCons ('HCons x ': xs) =  'HCons x ': 'HCons x ': Double xs
        DoubleNil 'HNil = 'HNil

[blacktriangle]

So totally different function, I meant by double to turn [1,2] into [2,4], however that's a really neat example. I hadn't seen the family extension in Haskell before. You're right there is a ton more to type systems than I was aware of. I was following some links in this thread and found this as well: https://www.parsonsmatt.org/2017/10/11/type_safety_back_and_....

I was less than impressed with type systems because like the blog post says, they tend to just kick the can down the road. The blog post uses a technique like you did in your example where rather than emitting more complicated type, they use the type system to protect the inputs of the function thus moving handling with the problem to the edges of the system which seems like a huge win. Between your example and that post I'm starting to see what people mean when they talk about programming in types, as its almost like the type system become a DSL with its own built-in test suite with which to program rather than a full programming language.

Either way very thought provoking, thank you for your responses.

[tsss]

> I meant by double to turn [1,2] into [2,4]

Hmm, I think you can do that too, but you'd have to assign each int value its own singleton type, which would be ridiculous and not gain you anything since you're just moving the logic up one level in the hierarchy of universes.

> what people mean when they talk about programming in types

If the type system is powerful enough then you can express any function at the type level. Some languages with universal polymorphism make no difference between types and terms. Any function can also be used at the type-level, kind-level and so on. Though usually just defining a simple wrapper type with smart constructor will get you 80% of the way in a business application with 2% of the effort of real type-level programming.