What Is Gradual Typing? (2009)(wphomes.soic.indiana.edu)
wphomes.soic.indiana.edu
What Is Gradual Typing? (2009)
https://wphomes.soic.indiana.edu/jsiek/what-is-gradual-typing/
35 comments
>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.
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...
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...
There is an advanced type system that is becoming more and more mainstream, it's Typescript.
E.g: https://www.typescriptlang.org/docs/handbook/advanced-types....
(conditional types for example)
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.
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.
What would runtime dependent types be? As I understand, they are a tool for statically proving properties of some code. What use are they at runtime? For code that came up as a result of the working system? I believe properties of generated programs can also be proven statically. For user-provided code? Why not just run the compiler/interpreter on it?
In practice, the overwhelming majority of tests I see in dynamic languages are just checking things that get statically checked in a language with a good algebraic type system (e.g. Typescript, Rust, Haskell, etc.)
The Rust type system made me understand why you want to have one.
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.
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 like it in principle, but it can also be really annoying and fussy. A lot of the time with Rust (perhaps because I'm no good, but still) I find myself fiddling around with some inane difference between two types I don't really care about (for instance, whether a function pointer is boxed or not). It gets so distracting that I often do the bulk of the work with the linter switched off, just so I can actually think about what I'm doing without having to go down a rabbit hole just so an option is turned into a result in some bit of the code I'm probably going to delete anyway.
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 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 think you probably are just not there yet, Rust defintly has a steep learning curve to it, especially if you are used to other paradigms or patterns than those used in the language.
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.
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.
I think python is a great example of what I'm talking about, though. I'm not a Python programmer - I've never written anything over a hundred lines in Python, nor sat down to really learn it. However, every time I do something in Python, I'm impressed by how smoothly what I expect to happen actually happens.
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.
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.
> 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...
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.
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.
[deleted]
Dependently typed languages are one example, but there are popular languages with modern type systems and various degrees of popularity. The ML-family comes to mind. Rust is one gaining traction as well.
Keep in mind Python was considered niche 10 years ago.
Keep in mind Python was considered niche 10 years ago.
I'd say Python was niche closer to 20 years ago. According to http://pypl.github.io/PYPL.html in 2009 Python was about as popular as C# is now, which is my recollection.
Advanced type systems can prove more complex properties of your program; there will theoretically always be properties we can't prove (by means of type systems or otherwise), and practically there will be properties that are too hard to prove. Even with dependent types, "essentially any" is an overstatement.
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.
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.
I considered writing "prove any property that is provable" but it is a tautology and doesn't convey the meaning I was trying to give it.
"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.
"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.
Yeah, I readily acknowledge that it's a nit. I didn't mean that portion of my comment as criticism of what you wrote, so much as rhetorical framing for my next point.
There will always be things we fundamentally can't prove, but those things have no place in a program you're relying on. "Essentially any" means that any you the programmer have reason to believe and code up.
If it's the property you need, and you can't prove it, it's still the property you need - you can't simply define it away.
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.
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.
> 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.
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.
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.
[Idris - Define a 'Prime' type](https://stackoverflow.com/q/46132987/5534735)
it looks pretty weird tbh. the ergonomics of dependent types are an open area of research
it looks pretty weird tbh. the ergonomics of dependent types are an open area of research
Jeremy’s co-author for the gradual typing series was Walid Taha—one of the principle creators of MetaOCaml. They are both top-notch programming language researchers.
> 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.
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.
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.
An important point of using dynamic types is not mentioned:
The actual workflow of coders: Compile, run, fail, repeat vs. eval, fail, repeat.
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.
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.
Interesting: I was first exposed to incremental development (in LOGO, Lisp and Smalltalk) in the 70s and found static languages painful and alien into the 90s, but have mostly flipped my preference.
I had a friend who described incremental programing as "programming by successive approximation". He wasn't praising it.
I had a friend who described incremental programing as "programming by successive approximation". He wasn't praising it.
Depends on the problem you're solving. That's a terrible way to write a filesystem, but a wonderful way to write a UI widget.
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.
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.
I might be misunderstanding, but it’s definitely possible to emulate this feedback loop with statically typed languages.
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.
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.
Most languages in the ML-family are statically typed and have a REPL.
I really hope that in the future gradual typing and dependent types can come together into an ergonomic to use system where we can let the compiler check/enforce proofs of correctness, but not require them. There's a ladder of correctness (simple type checks, unit tests, integration tests, proofs of different aspects of correctness) and each has a tradeoff vs effort. It would be really great to be about to be able to move around it without rewriting much code, but rather by adding more and more annotations as needed for your use.
A thread from 2014: https://news.ycombinator.com/item?id=8594079
2009: https://news.ycombinator.com/item?id=556794
2009: https://news.ycombinator.com/item?id=556794
I have some noob questions that I don't know how to ask:
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.
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.
Pattern matching can be used in typed and untyped languages.
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.
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.
This is an implementation of something similar on Smalltalk:
https://www.youtube.com/watch?v=1b3RRE9a8NA
If I understand correctly, most language supports gradual typing today (typescript, c++, rust, etc) through "any"
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.