I’ve come to the same conclusions. For me, the magic combination of features needed in a static type system is almost the same:
type inference everywhere (or almost everywhere)
algebraic data types (i.e. Sum/tagged union types, must be parameterizable i.e. generics, and have pattern matching)
soundness
immutability by default
These are not always enough by themselves. You need libraries and frameworks that build on these things in the right way. But when they are present, it seems the ecosystem naturally gets it right.
I think the key thing is this set of features enables you to “make illegal states unrepresentable” - and makes it less painful than the alternative ways of coding.
This doesn’t mean I only use languages like this. I actually use Python mainly, and it also has a completely different set of features that has its own set of advantages. In some cases these features produce ecosystems that are hard for statically typed languages to rival (e.g. the Django ecosystem).
But I do think if you only have experience of C/C++/C#/Java/TypeScript, you don’t know enough about type systems to dismiss the advantages of things like Elm/Haskell/OCaml/ReScript/Rust, which really do put you into a different world.
I think the key thing is this set of features enables you to “make illegal states unrepresentable”…
For me, this was how the value of static typing really “clicked” in my brain. I had understood very generally why people liked it for years, but it never seemed like that big a deal until I learned about sum types (although I guess enums started me down that line of thought).
Fwiw, TypeScript does actually have just about rich enough types to support for nice things like sum types - not directly but there’s an okay way to encode it.
With TypeScript, it’s the lack of soundness that lets you down, combined with the number of type annotations needed to get you to the point where you are confident that the compiler will always have your back. You start in a very different place to something like Elm. YMMV etc.
Yes. I think the richness of TS’ types still make it a meaningful win over JS, especially where they’ve pushed it over the last few years, but I also consistently miss the soundness of Rust, Elm, etc. when working with it.
I don’t feel that on a day to day basis the unsoundness is causing me big problems. It just means the type system has loopholes: you don’t poke them on purpose and it doesn’t come up. null safety is a much bigger deal and tsc gets that right.
It’s like, even in Haskell I can accidentally write an infinite loop and it’ll almost certainly type check since let x = x in x has type forall a. a. IME that’s about 50% “just don’t do that, then” plus 50% “explicit recursion is slightly perilous so write everything as map+foldr invocations”.
I went through a similar process, from being a massive Smalltalk fan (and implementing an AoT-compiled Smalltalk) to working on a language with a static type system. The things that make me hate static types in languages were largely coming from the Pascal view of the world, where the types aren’t sufficiently expressive to check the invariants that I do get wrong or to be able to understand things that I knew were correct. In languages like Pascal (and, often, C++), I need type-system escapes because I can’t express exactly what I want in the type system and so it raises false positives (this is safe, but you need a reinterpret_cast) and false negatives (this is unsafe, but the type system still allows it).
My list (i.e. what we’ve converged on for Verona, which is not what I originally wanted but what other people have convinced me that I now want) is similar to yours:
Complete type inference within a function, but fully specified types on function boundaries. Global type inference is both complex for the compiler and for the programmer, because I have to run the type inference algorithm in my head over the whole program to understand the types at a specific point.
No magic types (anything that has a type that can be inferred should have a type that I can write down using the language syntax. If it’s hard for the reader to figure out a type then I should be able to write it explicitly.
Structural types. Concrete types that implement a set of methods implement any interface that matches that set of methods.
Algebraic types. Union and intersection types are both incredibly useful. Union types let me pass around something that must be one of a small set of things. Intersection types on interfaces let me match on things that implement multiple behaviours easily. That gives me most of what I enjoy from dynamic languages in the Smalltalk family but in a way that is much easier to optimise.
Flow sensitivity. If I write if (x is T) then I shouldn’t need to cast x to T in the body of that if statement. Any code in blocks that are dominated by that check should assume that the type of x is T. The same applies to pattern matching on types. If I nest pattern matching on interface types, the type in the nested block should be an intersection type of both interfaces.
Immutability and ownership as first-class components of the type system. If I want an immutable string, I can write imm & String (intersection type that must be both immutable and String). In Verona, ownership is tied to regions. Any pointer is either imm (can’t be modified by anyone), iso (is the only pointer from outside a region to the sentinel object that dominates all objects in a region), mut (is an interior pointer to an object in a region, can be stored only on the stack or in a field of another object in the region), or readonly (may be any of the above, but I cannot modify it via this pointer).
Generics.
Rich compile-time reflection in the language, which I can use to implement run-time reflection on the types and properties that I want (ideally using standard-library types).
I’m not a fan of immutability by default because it then requires a lot of careful optimisation in the compiler to figure out when it’s safe to do in-place mutation and that leads to performance that’s very hard to reason about. The Verona model for immutability is that every object is created mutable (either as the sentry of a new region or in the same region as some other object) but if you have an iso pointer to the sentinel of a region, you can freeze that region. You then get an immutable object graph, which may contain cycles. Immutability is a distinct property to the object type.
This system makes it very easy to express the invariant that any only immutable objects can be shared between threads (which is the number one property I want my type system to enforce) and makes it cheap to pass complex (possibly cyclic) object graphs between threads without needing any type-system escapes (this is possible in Rust only by using unsafe crates - even passing a DAG between two threads in Rust requires using something like the RC trait, which is implemented in unsafe).
We use Mypy with Python 3 extensively. The type system (of which Mypy is simply one implementation) is expressive, elegant, and captures the kinds of problems we want to solve very well. We get to use Python’s extensive standard library and large ecosystem with strong, compile-time-checked typing.
That being said, we went this route because a huge amount of our code was already written in Python. If we had started from scratch, we probably would’ve gone with Rust. I might still try to toss some Rust in there; I’m not a huge Rust fan yet, but it’s growing on me.
To those who want to open their eyes about the power of using types in programming, Cardelli’s “Typeful Programming” is a strongly recommended reading. :)
Yes! As an early engineer my opinion on types was most easily summarized as “they get in the way”. But, oh, wow, was I wrong.
If you accept compile time errors as a provocation to re-think your code, you will see many benefits from security, reliability to cleaner architecture.
I’ve come to the same conclusions. For me, the magic combination of features needed in a static type system is almost the same:
These are not always enough by themselves. You need libraries and frameworks that build on these things in the right way. But when they are present, it seems the ecosystem naturally gets it right.
I think the key thing is this set of features enables you to “make illegal states unrepresentable” - and makes it less painful than the alternative ways of coding.
This doesn’t mean I only use languages like this. I actually use Python mainly, and it also has a completely different set of features that has its own set of advantages. In some cases these features produce ecosystems that are hard for statically typed languages to rival (e.g. the Django ecosystem).
But I do think if you only have experience of C/C++/C#/Java/TypeScript, you don’t know enough about type systems to dismiss the advantages of things like Elm/Haskell/OCaml/ReScript/Rust, which really do put you into a different world.
For me, this was how the value of static typing really “clicked” in my brain. I had understood very generally why people liked it for years, but it never seemed like that big a deal until I learned about sum types (although I guess enums started me down that line of thought).
Fwiw, TypeScript does actually have just about rich enough types to support for nice things like sum types - not directly but there’s an okay way to encode it.
With TypeScript, it’s the lack of soundness that lets you down, combined with the number of type annotations needed to get you to the point where you are confident that the compiler will always have your back. You start in a very different place to something like Elm. YMMV etc.
Yes. I think the richness of TS’ types still make it a meaningful win over JS, especially where they’ve pushed it over the last few years, but I also consistently miss the soundness of Rust, Elm, etc. when working with it.
I don’t feel that on a day to day basis the unsoundness is causing me big problems. It just means the type system has loopholes: you don’t poke them on purpose and it doesn’t come up.
nullsafety is a much bigger deal and tsc gets that right.It’s like, even in Haskell I can accidentally write an infinite loop and it’ll almost certainly type check since
let x = x in xhas typeforall a. a. IME that’s about 50% “just don’t do that, then” plus 50% “explicit recursion is slightly perilous so write everything as map+foldr invocations”.I went through a similar process, from being a massive Smalltalk fan (and implementing an AoT-compiled Smalltalk) to working on a language with a static type system. The things that make me hate static types in languages were largely coming from the Pascal view of the world, where the types aren’t sufficiently expressive to check the invariants that I do get wrong or to be able to understand things that I knew were correct. In languages like Pascal (and, often, C++), I need type-system escapes because I can’t express exactly what I want in the type system and so it raises false positives (this is safe, but you need a
reinterpret_cast) and false negatives (this is unsafe, but the type system still allows it).My list (i.e. what we’ve converged on for Verona, which is not what I originally wanted but what other people have convinced me that I now want) is similar to yours:
if (x is T)then I shouldn’t need to castxtoTin the body of that if statement. Any code in blocks that are dominated by that check should assume that the type ofxisT. The same applies to pattern matching on types. If I nest pattern matching on interface types, the type in the nested block should be an intersection type of both interfaces.imm & String(intersection type that must be both immutable and String). In Verona, ownership is tied to regions. Any pointer is eitherimm(can’t be modified by anyone),iso(is the only pointer from outside a region to the sentinel object that dominates all objects in a region),mut(is an interior pointer to an object in a region, can be stored only on the stack or in a field of another object in the region), orreadonly(may be any of the above, but I cannot modify it via this pointer).I’m not a fan of immutability by default because it then requires a lot of careful optimisation in the compiler to figure out when it’s safe to do in-place mutation and that leads to performance that’s very hard to reason about. The Verona model for immutability is that every object is created mutable (either as the sentry of a new region or in the same region as some other object) but if you have an
isopointer to the sentinel of a region, you can freeze that region. You then get an immutable object graph, which may contain cycles. Immutability is a distinct property to the object type.This system makes it very easy to express the invariant that any only immutable objects can be shared between threads (which is the number one property I want my type system to enforce) and makes it cheap to pass complex (possibly cyclic) object graphs between threads without needing any type-system escapes (this is possible in Rust only by using
unsafecrates - even passing a DAG between two threads in Rust requires using something like theRCtrait, which is implemented inunsafe).We use Mypy with Python 3 extensively. The type system (of which Mypy is simply one implementation) is expressive, elegant, and captures the kinds of problems we want to solve very well. We get to use Python’s extensive standard library and large ecosystem with strong, compile-time-checked typing.
That being said, we went this route because a huge amount of our code was already written in Python. If we had started from scratch, we probably would’ve gone with Rust. I might still try to toss some Rust in there; I’m not a huge Rust fan yet, but it’s growing on me.
Set is one of the most basic (mathematical) concepts one must have in order to abstractly reason.
Then, types, which are a refinement over sets.
To those who want to open their eyes about the power of using types in programming, Cardelli’s “Typeful Programming” is a strongly recommended reading. :)
Yes! As an early engineer my opinion on types was most easily summarized as “they get in the way”. But, oh, wow, was I wrong.
If you accept compile time errors as a provocation to re-think your code, you will see many benefits from security, reliability to cleaner architecture.
Do tell, what untyped languages have you worked in.
Are there dynamic types adepts left on this planet?