5 ms·

I am in general deeply skeptical of gradual typing, partially from my own underwhelming experiences with MyPy, and partially because 99% of the time when I hear

I am in general deeply skeptical of gradual typing, partially from my own underwhelming experiences with MyPy, and partially because 99% of the time when I hear someone advocating for them, they (1) take as given that dynamic typing makes for more productivity (which does not reflect my own experience), and therefore don't try to justify the claim at all, and (2) they say what gradually types give you is not having to annotate things up front. Types have not required manual annotations since at least 1978 (the original hindley-milner type system which, I will note, while not new, is still more recent than prolog). TFA does all of the above, plus a parenthetical saying "inference is addressed in the next section" -- and then does not actually address inference later in the post. I'd much rather have type inference than optional typing.

catnaroek 9y ago
The argument for dynamic typing (whether one agrees with it or not, I actually don't) has nothing to do with explicit annotations. Rather, it is that there are paths in the design space that lead to correct solutions but pass through several inconsistent attempts (i.e., containing parts that contradicting each other and/or the problem statement). It is useful (again, according to proponents, not me) to consider these inconsistent attempts valid programs so that programmers can obtain example-based feedback about the consequences of their designs. Logic and abstract reasoning are not everyone's forte, after all.
- zenhack 9y ago
  Yeah, that's an actually reasonable argument (I don't buy it either, but it's coherent enough). But I honestly think most of the time people aren't making that argument, they're just complaining about the typed languages they know -- more often than not Java.
  - mcphage 9y ago
    > they're just complaining about the typed languages they know -- more often than not Java. Java has a particularly bad type system, and it used to be even worse.
- winstonewert 9y ago
  I'd make yet a different account of the benefit of dynamic typing. My reasoning skills exceed that of my compiler and I can thus determine that certain designs are type-safe that my compiler cannot. This means that in static languages I end up either 1) spending a lot of time convincing the compiler my design is type-safe, 2) am restricted in the designs I can choose 3) casting types losing the advantage of static typing. With dynamic typing I'm free to just write the code. Having said that, I now really like Rust which goes all the way in the other direction.
  - catnaroek 9y ago
    This is a very good argument against mandatory automatic static checks, so long as they are replaced with equally mandatory manual proofs, included in the program's comments and/or documentation. But it does not justify dynamic typing in any way. For example, most programming languages offer no way to statically verify array indexing operations, so I just get my hands dirty and prove my array indices correct the old fashioned way (brain, paper and pen). But runtime bounds checking still annoys me, because they branch on a bit whose value I know beforehand, creating an unreachable control flow path.
    - winstonewert 9y ago
      Are you telling me that you do a formal proof on pen and paper for every array index to ensure that it is valid?
      - catnaroek 9y ago
        Yes. This is the only way you can justify that you know better than the compiler.
        winstonewert 9y ago
        So, if you wrote the following code: double sum(double[] numbers) { double total = 0.0; for (int index = 0; index < numbers.length; index++) { total += numbers[index]; } return total } You would write a formal proof on paper that the index won't go out of bounds?
wcrichton 9y ago
Apologies, I forgot to follow up on the promised inference discussion in the original version of the post. I just added a paragraph at the end on my thoughts. > Another big question in gradual programming is inference vs. annotation. As our compilers get smarter, it becomes easier for information like types, lifetimes, and so on to be inferred by the compiler, even if not explicitly annotated by the programmer. However, inference engines are rarely perfect, and when they don't work, every inference-based language feature (to my knowledge) will require an explicit annotation from the user, as opposed to simple inserting the appropriate dynamic checks. In the limit, I envision gradual systems have three modes of operation: for any particular kind of program information, e.g. a type, it is either explicitly annotated, inferred, or deferred to runtime. This is in itself an interesting HCI question--how can people most effectively program in a system where an omitted annotation may or may not be inferred? How does that impact usability, performance, and correctness? This will likely be another important avenue of research for gradual programming. This is to say, I don't think inference and gradual systems are necessarily at odds, but could potentially work together, although that doesn't happen today. Additionally, I didn't want to dive into dynamic vs. static typing at risk of inflaming the Great War, but the point I was trying to make was moreso empirical. A huge number of programmers have used dynamic languages to build large systems in the last two decades, which suggests that there is _some_ benefit, although further research is needed to precisely quantify the benefit of dynamic languages.
- catnaroek 9y ago
  > This is to say, I don't think inference and gradual systems are necessarily at odds, but could potentially work together, although that doesn't happen today. Type inference demands some rigidity in the type structure of a language. You must have the right amount of polymorphism: the STLC has too little, System F has too much. If you want both type operators and type synonyms, then operators can't be applied to partially applied synonyms [0], because higher-order unification is undecidable. If you want subtyping, you also have to do it in a certain way [1]. More generally, the type language must have a nice enough algebraic structure to make it feasible to solve systems of type (in)equations, because that's how inference works. Your post contains a link to a paper [2] that contains the following passage: > In this paper, we present a way to achieve efficient sound gradual typing. The core component of this approach is a nominal type system with run-time type information, which lets us verify assumptions about many large data structures with a single, quick check. I have no way to confirm this claim at the moment, but it seems entirely reasonable. Checking structural types requires doing more work. But it is this very structure that makes type inference possible and useful. So, yes, it seems that inference and gradual typing will be difficult to reconcile. --- Footnotes: [0] http://cstheory.stackexchange.com/questions/32260/ http://cstheory.stackexchange.com/questions/32260/ (I am the author of this stupid question.) [1] http://news.ycombinator.com/item?id=13781467 http://news.ycombinator.com/item?id=13781467 [2] http://www.cs.cornell.edu/~ross/publications/nomalive/nomalive-oopsla17.pdf http://www.cs.cornell.edu/~ross/publications/nomalive/nomali...

catnaroek 9y ago

The argument for dynamic typing (whether one agrees with it or not, I actually don't) has nothing to do with explicit annotations. Rather, it is that there are paths in the design space that lead to correct solutions but pass through several inconsistent attempts (i.e., containing parts that contradicting each other and/or the problem statement). It is useful (again, according to proponents, not me) to consider these inconsistent attempts valid programs so that programmers can obtain example-based feedback about the consequences of their designs. Logic and abstract reasoning are not everyone's forte, after all.

zenhack 9y ago
Yeah, that's an actually reasonable argument (I don't buy it either, but it's coherent enough). But I honestly think most of the time people aren't making that argument, they're just complaining about the typed languages they know -- more often than not Java.
- mcphage 9y ago
  > they're just complaining about the typed languages they know -- more often than not Java. Java has a particularly bad type system, and it used to be even worse.
winstonewert 9y ago
I'd make yet a different account of the benefit of dynamic typing. My reasoning skills exceed that of my compiler and I can thus determine that certain designs are type-safe that my compiler cannot. This means that in static languages I end up either 1) spending a lot of time convincing the compiler my design is type-safe, 2) am restricted in the designs I can choose 3) casting types losing the advantage of static typing. With dynamic typing I'm free to just write the code. Having said that, I now really like Rust which goes all the way in the other direction.
- catnaroek 9y ago
  This is a very good argument against mandatory automatic static checks, so long as they are replaced with equally mandatory manual proofs, included in the program's comments and/or documentation. But it does not justify dynamic typing in any way. For example, most programming languages offer no way to statically verify array indexing operations, so I just get my hands dirty and prove my array indices correct the old fashioned way (brain, paper and pen). But runtime bounds checking still annoys me, because they branch on a bit whose value I know beforehand, creating an unreachable control flow path.
  - winstonewert 9y ago
    Are you telling me that you do a formal proof on pen and paper for every array index to ensure that it is valid?
    - catnaroek 9y ago
      Yes. This is the only way you can justify that you know better than the compiler.
      - winstonewert 9y ago
        So, if you wrote the following code: double sum(double[] numbers) { double total = 0.0; for (int index = 0; index < numbers.length; index++) { total += numbers[index]; } return total } You would write a formal proof on paper that the index won't go out of bounds?

wcrichton 9y ago

Apologies, I forgot to follow up on the promised inference discussion in the original version of the post. I just added a paragraph at the end on my thoughts. > Another big question in gradual programming is inference vs. annotation. As our compilers get smarter, it becomes easier for information like types, lifetimes, and so on to be inferred by the compiler, even if not explicitly annotated by the programmer. However, inference engines are rarely perfect, and when they don't work, every inference-based language feature (to my knowledge) will require an explicit annotation from the user, as opposed to simple inserting the appropriate dynamic checks. In the limit, I envision gradual systems have three modes of operation: for any particular kind of program information, e.g. a type, it is either explicitly annotated, inferred, or deferred to runtime. This is in itself an interesting HCI question--how can people most effectively program in a system where an omitted annotation may or may not be inferred? How does that impact usability, performance, and correctness? This will likely be another important avenue of research for gradual programming. This is to say, I don't think inference and gradual systems are necessarily at odds, but could potentially work together, although that doesn't happen today. Additionally, I didn't want to dive into dynamic vs. static typing at risk of inflaming the Great War, but the point I was trying to make was moreso empirical. A huge number of programmers have used dynamic languages to build large systems in the last two decades, which suggests that there is _some_ benefit, although further research is needed to precisely quantify the benefit of dynamic languages.

catnaroek 9y ago
> This is to say, I don't think inference and gradual systems are necessarily at odds, but could potentially work together, although that doesn't happen today. Type inference demands some rigidity in the type structure of a language. You must have the right amount of polymorphism: the STLC has too little, System F has too much. If you want both type operators and type synonyms, then operators can't be applied to partially applied synonyms [0], because higher-order unification is undecidable. If you want subtyping, you also have to do it in a certain way [1]. More generally, the type language must have a nice enough algebraic structure to make it feasible to solve systems of type (in)equations, because that's how inference works. Your post contains a link to a paper [2] that contains the following passage: > In this paper, we present a way to achieve efficient sound gradual typing. The core component of this approach is a nominal type system with run-time type information, which lets us verify assumptions about many large data structures with a single, quick check. I have no way to confirm this claim at the moment, but it seems entirely reasonable. Checking structural types requires doing more work. But it is this very structure that makes type inference possible and useful. So, yes, it seems that inference and gradual typing will be difficult to reconcile. --- Footnotes: [0] http://cstheory.stackexchange.com/questions/32260/ http://cstheory.stackexchange.com/questions/32260/ (I am the author of this stupid question.) [1] http://news.ycombinator.com/item?id=13781467 http://news.ycombinator.com/item?id=13781467 [2] http://www.cs.cornell.edu/~ross/publications/nomalive/nomalive-oopsla17.pdf http://www.cs.cornell.edu/~ross/publications/nomalive/nomali...