What Is Gradual Typing? (2009)
wphomes.soic.indiana.edu
wphomes.soic.indiana.edu
Bad bad point. There are statically-typed languages with fairly complex type systems. There are even dependently typed languages which check essentially any property of you values and can be used to prove your program correct.
> Most of the work in making sure that your program is correct [...] goes into developing comprehensive tests.
Tests can only show the presence of bugs, never the absence of them. This is not me speaking, this is Dijkstra.
It is ok to prefer one method over the other, but there's clearly an aura of opinion on the statements of this article. It would be better for the reader to explicitly differentiate fact from opinion there.
An introductory discussion such as this is better kept at languages / type systems people actually use, not what might be possible, or whatever academic or niche stuff is out there.
Dependent types are totally academic/enthusiast concern at this point, Haskell is still very much niche, and only Rust might cut it as having a slightly more complex type system and being actually used...
So, this would be like correcting a post about modern music for failing to include "12-tone Nordic heavy metal-afrobeat ragas" that all 3 bands with 200 fans altogether listen to...
Also c++20 with concepts will push the boundaries of what is possible.
But what I'm really looking for and doesn't exist except maybe through libraries, is runtime Dependant types.
It boils down to beeing able to catch as many bugs as possible in compile time and a good type system allows you to move whole classes of rules into that space.
So when you try to use that variable wirh the wrong type in the wrong place it will notify you before deployment. This can be extremely reassuring and allows you to code more freely because it makes it harder to break things accidentally in a bad way.
I think a combination of the explicitness about performance implications, the focus on safety, and the whole lifetime thing leads to Rust being, if not specifically complicated to write, at least extremely fiddly. Which is great if you're in some kind of hot spot where you need all that control and safety. But when you're just trying to add two strings together to make some random error message, it's actually really annoying having the language purposefully complicate things just so you realize there's going to be an allocation. It leads to a really weird distribution of effort, where I spend about half the time on important stuff, and the other half on things that are so trivial and irrelevant to both performance and user experience that I'd be totally happy if they were just all dumped on the heap and cast through void pointers.
I remember fighting the compiler because I tried to write what I thought of as “beautiful” abstractions, that were basically inspired by my object oriented Python use. Everything and the interaction between everything was a incredibly hard challenge. Until at one point I just gave up and said: “Okay Rust, scrap beautiful code, I’ll just do it your way” and then things started instantly to fall into place.
I am not saying that this is where you are at, but it was like that for me. Do I still struggle with types? Sometimes, but rarely and then it is mostly a mix between lack of focus, lazyness and a mistake somewhere else.
With Rust, where I've put in a chunk of effort to learn, where I've read books, and have written a substantial amount of code, I'm constantly going back to the documentation to do simple things. The main offender is my inability to remember what traits are implemented by what types. I mean, off the top of your head, is '.binary_search()' a method on &[T] or Vec<T>? Or both? I literally can't remember right now.
They're also sneaking into the gradually typed languages. Typescript and python both support literal types, which are a (very) weak form of dependent types. C++ templates also support a different weak form of dependent types (ints), that is used to, among other things, support typechecked matrix operations in eigen.
Keep in mind Python was considered niche 10 years ago.
But often times you can make important and hard-to-reason-about properties of your system "simple" from the perspective of the type system. For example, I used the C type checker to help make sure I was calling functions from the correct thread. I have a talk about it I've given a couple times - slides as C files here: https://github.com/dlthomas/using-c-types-talk/tree/master/s... - with an example program where the technique turns an occasional segfault at runtime into a "you can't call this here, dummy" error at compile time.
"Essentially any" can be better stated indeed as it is too broad, but I can't think of a definition right now that doesn't require a few pages of text.
As I said, though, you'll almost always be hitting practical limits long before theoretical ones.
And as I also said, there's still quite a few useful things we can speak meaningfully about, even in a quite impoverished setting.
Which are those languages? Can you show me how to use dependent typing to ensure that an integer is a prime number in such a language? Because I don't think you can do that, at least not using convenient syntax.
it looks pretty weird tbh. the ergonomics of dependent types are an open area of research
True, but that shifts the "bad point" to difficulty writing your program in a provable correct way.
Static typing in Java is as different from static typing in Coq as it is from static typing Bash (i.e. none).
The comparison is a simplified one.
After over 35 years of coding - mostly with statically compiled languages -doing it REPL-style makes such an enormous difference in my enjoyment of the profession. I'm not sure I can go back to a compiler.
I had a friend who described incremental programing as "programming by successive approximation". He wasn't praising it.
It's hard to reason from first principles how much padding should be between items in a list, or how fast a spinner should spin.
For example, Haskell has the `-fdefer-type-errors` flag that will turn type errors into warnings at compile time and runtime failures if the expression that fails to type-check is evaluated.
What, if any, is the relationship between type systems and pattern matching?
Does structural typing reduce the need for instanceof style tests?
So if a language uses structure typing, is pattern matching not useful, applicable?
--
Thanks for humoring me. I'm mostly a Java programmer, self taught, no CS background. I've been reading wiki articles about type systems, trying to figure out what it all means, how to get started. Inference, structural vs nominal, linear types... But, honestly, my eyes glaze over pretty quickly.
Am planning on powering thru Appel's 2002 book, especially implementing the type system, but we'll see how far I get.
One reason it's more strongly associated with typed languages is that the type system can easily check a pattern match to prove various things about it (e.g. that the set of pattern matches covers all possible inputs).
Note that there is no technical reason an if/then/else construct couldn't be used instead, but the shape of the data is front and center with a pattern match.