"This brings another discussion point: a type system naturally restricts the amount of code we can write because, in order to prove certain properties about our code, certain styles have to be rejected."
I can't but think few things:
- by compilers (in this case static type checkers) laws we all know that there are valid programs that won't satisfy the type checker and viceversa there's only a handful (none being production or development ready) of compilers powerful enough to infer all code bugs
- limiting the expressiveness of a language isn't necessarily a bad thing
I've noticed that people with a huge background in dynamic languages tend to have a natural refusal for static types. Lispers are a community with such an attitude, even the typed lisps like typed/racket seem to be born more to please people wanting typecheckers and academics than the userbase itself.
But I, and my mind, work the other way around: I want to think about the types first, I need them to express my domain and my DSLs, so I need an expressive type system able to translate my thoughts and validate all of my program with nothing but types. It's possible in plenty of languages (most famous one is TypeScript with its declare keyword) to do type-driven development and I can't really function without it.
Once a program has been well modeled, once I've seen the APIs, then and only then I get into implementation and it is by far the part I spend less time on.
Every time I read a lisp dialect without static types (most of them) my mind just doesn't work properly, I can't follow much. And I really believe that the lack of commercial success for many of these languages derives from how poorly non statically-typed languages scale when klocs and number of maintainers of a project start increasing.
The main question of the quote is: if we introduce a system that rejects a "large" amount of Elixir code, will developers adopt it? If some language features are only available for "untyped" code, will developers often forego types only to get those features? And if that happens, could we end-up "forking" the Elixir community, where part of the community uses some idioms and the other part uses others (which is a common complaint about large languages)?
The goal is not to reject types but rather to find a theory that mirrors the language as close as possible. I believe balancing these trade-offs will be essential to the adoption and success of a type system in Elixir.
I use Elixir whenever I can, and I would love a better type system (though I admittedly suck at using what Dialyzer already provides, which is extensive). I'm very excited to see where the current effort goes!
But absolutely, if new types break existing Elixir code and idioms it would result in a schism that would be devastating and disastrous to the Elixir community. I for one am really glad you are asking these questions, and FWIW I think you're doing exactly the right thing.
> I've noticed that people with a huge background in dynamic languages tend to have a natural refusal for static types. Lispers are a community with such an attitude, even the typed lisps like typed/racket seem to be born more to please people wanting typecheckers and academics than the userbase itself.
I feel like it's the opposite. It seems like we have this huge wave of a push for static types. The only way I can explain it to myself is that a bunch of people using dynamically typed languages finally came over to the static typing side. And I say this as someone that worked using statically typed languages for pretty much all of their career.
I get it for TypeScript and the frontend. The frontend is a huge, complex mess of interactions, in the same codebase. Static types are awesome there.
But the way we write most backend systems these days, IMHO, static types are practically a nothingburger. Sure, they were awesome when I was working on those millions of LOC projects back in the 2000s. But nowadays those millions of locs are spread across N projects which are separated by a typeless network boundary so I'm not looking at anything more than 50-100k LOC anyways.
So I just don't get it. Systems are written in a way that devalues static typing, but it feels like the demand for it is higher than ever.
As someone maintaining a moderately complex codebase in Python: static typing doesn't feel valuable until you need it. But then you really, really need it. Thank god for Mypy and type-hints.
I'd prefer something that can infer types in the simple case and have explicit types when dealing with huge complexity. Really, it comes down to having tight control around the shapes of your data, and that is incredibly valuable when you cannot keep the entire codebase/API/contract in your head. Quick navigation is a huge bonus too.
I also don't fully understand it. Maybe it's driven more by the ease of autosuggesting/completing in static typed languages than actually catching bugs. It will swing back like everything else and reorient on slightly different direction. This pendulum is quite slow though.
It's not satisfying to everyone, but if lack of types is hampering your desire to learn Elixir, check out Dialyzer[1]. It's certainly not perfect, but between pattern matching struct arguments and Dialyzer, I've yet to personally encounter a situation where it wasn't sufficient.
Programs never have to be rejected; programs can be diagnosed (so we are informed) and run anyway.
Programs have to be rejected if there is no safe way to handle them at run-time, when for the sake of efficiency we removed the type bits from the data. (And not even always then; the programmer may have assured safety otherwise.)
Every time I read statements like this from Jose
"This brings another discussion point: a type system naturally restricts the amount of code we can write because, in order to prove certain properties about our code, certain styles have to be rejected."
I can't but think few things:
- by compilers (in this case static type checkers) laws we all know that there are valid programs that won't satisfy the type checker and viceversa there's only a handful (none being production or development ready) of compilers powerful enough to infer all code bugs
- limiting the expressiveness of a language isn't necessarily a bad thing
I've noticed that people with a huge background in dynamic languages tend to have a natural refusal for static types. Lispers are a community with such an attitude, even the typed lisps like typed/racket seem to be born more to please people wanting typecheckers and academics than the userbase itself.
But I, and my mind, work the other way around: I want to think about the types first, I need them to express my domain and my DSLs, so I need an expressive type system able to translate my thoughts and validate all of my program with nothing but types. It's possible in plenty of languages (most famous one is TypeScript with its declare keyword) to do type-driven development and I can't really function without it.
Once a program has been well modeled, once I've seen the APIs, then and only then I get into implementation and it is by far the part I spend less time on.
Every time I read a lisp dialect without static types (most of them) my mind just doesn't work properly, I can't follow much. And I really believe that the lack of commercial success for many of these languages derives from how poorly non statically-typed languages scale when klocs and number of maintainers of a project start increasing.