11 ms·

Is Sound Gradual Typing Dead? [pdf]

74 points by bshanks 11y ago

deleted 11y ago
[deleted]
- johnbender 11y ago
  It's worth noting that this is a peer reviewed conference publication (in POPL no less). So, despite the title a lot of time and thought has gone into the content.
tacos 11y ago
"We find that Typed Racket’s cost of soundness is not tolerable. If applying our method to other gradual type system implementations yields similar results, then sound gradual typing is dead." While some of the data is surprising (22x average slowdown for TypeScript dropping to 6.5% overhead when fully typed) the paper ignores the reason why people kicked and screamed for the functionality to begin with. It had nothing to do with run-time performance. Obviously the tools will improve and you can always strip out the annotations if performance is an issue. Reticulated Python is still an order of magnitude faster than Ruby, so obviously performance doesn't render a technology "dead."
- taylorfausak 11y ago
  > the paper ignores the reason why people kicked and screamed for the functionality to begin with No it doesn't. The explicitly talk about this in section 7: "The acceptance of Typed Racket in the commercial and open-source Racket community suggests that (some) programmers find a way around the performance bottlenecks of sound gradual typing." > Reticulated Python is still an order of magnitude faster than Ruby Are you suggesting that a slower variant of Python is ten times faster than Ruby? That doesn't match my experience. For what it's worth, Ruby outperforms Python in some benchmarks: http://benchmarksgame.alioth.debian.org/u64q/ruby.html http://benchmarksgame.alioth.debian.org/u64q/ruby.html
  - Veedrac 11y ago
    Looking at the first benchmark in the list you gave, just in-lining eval_A in the Python code (as the Ruby code does) makes the Python code competitive with the Ruby. As usual, don't trust the Benchmarks Game; it's not nearly well enough controlled to be a useful data point. (I do agree with your main point, though. CPython ain't that fast.)
    - igouy 11y ago
      As usual, don't trust Joshua Landau: without in-lining eval-A the Ruby code only slows from 102secs to 137secs. As usual, Joshua -- Do the ordinary thing and report specific programs that you think should not be allowed.
      - Veedrac 11y ago
        For those not aware, igouy maintains the Benchmarks Game.
        igouy 11y ago
        Nothing hidden about that -- http://benchmarksgame.alioth.debian.org/sometimes-people-just-make-up-stuff.html#history http://benchmarksgame.alioth.debian.org/sometimes-people-jus... How to report specific programs that you think should not be allowed -- http://benchmarksgame.alioth.debian.org/play.html#invalid http://benchmarksgame.alioth.debian.org/play.html#invalid
- sitkack 11y ago
  Are you referring to this paper? http://wphomes.soic.indiana.edu/jsiek/files/2014/08/retic-python-v3.pdf http://wphomes.soic.indiana.edu/jsiek/files/2014/08/retic-py...
  - tacos 11y ago
    As referenced in the paper itself, section 6.1.
    - igouy 11y ago
      For those who have not looked at the referenced paper, the last section is -- "6. Conclusions" "…Reticulated programs perform far worse than their unchecked Python implementation…" p10 "Design and Evaluation of Gradual Typing for Python"
      - sitkack 11y ago
        And I would argue that _use-site checking_ is the easiest and obviously the slowest method to attain the stated goal. Python is already slow, this is just going to make things silly. Using the same inference methods as Shedskin [0] along with type annotations, functional tests and property based testing can get both correctness and performance in a gradual layered manner. This paper doesn't prove that gradual typing is broken, it shows that _use-site checking_ happens to be slow for the version of Python that they used (PyPy could very well elide the checks). [0] Shedskin Thesis http://mark.dufour.googlepages.com/shedskin.pdf http://mark.dufour.googlepages.com/shedskin.pdf Iterative Flow Analysis by Plevyak http://plevyak.com/ifa-submit.pdf http://plevyak.com/ifa-submit.pdf Agesen's Cartesian Product http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.88.663&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.88....
        igouy 11y ago
        My point was simply that there is no section 6.1 in that paper, and what is in the paper does not support `tacos` claim ;-)
- deleted 11y ago
  [deleted]
kazinator 11y ago
> When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. Assertion without evidence. Lack of static typing is awesome in evolving a system: you can convert a part of it to some new types as "proof of concept" and still load and run the code to get usefully far. You just avoid stepping on the parts which aren't converted/refactored yet. Having something Working Now (tm) is a great motivator for some developers to keep going; it reduces the "activation potential barriers" against creativity. The trick to using dynamic languages is to have a ton of static experience. The typing is in your head, where it doesn't get in the way. What we are seeing a lot of lately is a crop of developers who have never worked in anything but some dynamic language. When I'm working in a dynamic language, my concept of type is consciously coming from all the static experience. That keeps me from doing totally scatter-brained things which are possible. I write code such that most of it could statically check, but with the freedom that some of it doesn't have to. Moreover, I am aware (hopefully!) of which code that is.
- vox_mollis 11y ago
  Lack of static typing is awesome in evolving a system I really don't follow your logic, here. Few things change more frequently while evolving/hacking together software than the data structures and types. Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems. If anything, it's the evolving/hacking process that's MOST prone to accumulating runtime type errors than any other process.
  - kazinator 11y ago
    > Few things change more frequently while evolving/hacking together software than the data structures and types. I tend to agree; it is often correct. (Though sometimes we have solid data structures and types and are able to evolve things without changing them.) Anyway, therefore it follows that if we calcify and ossify data structures and types, we kill the progress, not to mention fun. > Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems. This is blown out of reasonable proportion by static type advocates. In a dynamic system, type is de facto a few bits of value in an object. So the above situation is just another value that is wrong. Static programs also have run-time values that can be wrong. A static program that is supposed to calculate 42 might calculate 43, which has the correct type. To discover the cause, someone will have to sit down and think about the code. Code which has never been exercised by a test case (coverage) should still be regarded as garbage, in spite of passing type checking. It is not known to be correct. Type checked is not the same thing as correct. The graph of "type-value" in typical code is rather trivial. Take any moderately complex algorithm, and ignore what its operations are doing; just consider their input and output types. The resulting graph/tree is a lot simpler than what is going on with the values. Type problems are trivial. That is why it's even possible to move them to compile time and have static languages. Think about it: something that runs for hours or days in order to produce a result (and is not even known to terminate) can be entirely type-checked in a millisecond. We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling. The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking. Or it could sort them in descending order when the expected order is ascending: some test was reversed and the reverse test type checks because the operator is commutative. You still have to either prove your code if possible and feasible, else test it exhaustively if possible, or else test it imperfectly.
noelwelsh 11y ago
I love the work of the PLT group, and wish I had time to give this a better read right now. Barring that, I'll just waffle on related topics. Having worked for about a decade in dynamically typed languages (mostly Racket, with a bit of Ruby and Python) and about the same in modern statically typed languages (mostly Scala, with a bit of O'Caml) I've come to believe that the use of types is more a cultural issue than a technology one at this point in time. Let me attempt to explain. Working in Scala I've come to lean heavily on abstractions like applicatives and monads. When I design systems I now find I naturally break them down into these building blocks. For instance, a stream processing system I've been working on is an applicative functor (though I considered alternate designs that are Kleislis). Error handling is usually a monad. The meaning of the names doesn't matter. The important point I'm building systems by sticking together patterns. The patterns are different to OO design patterns as in the Gang-of-four book, but the core idea is the same. When I was more into dynamic types I didn't lean on patterns so much. I tended to hand design the abstractions in each component, and they didn't always fit together so well as a result. Why the difference? I have a few thoughts. Firstly, I've learned more with time. That's undeniable. But, more importantly, functional patterns have a different feel to OO patterns. They are much more precisely defined, with algebraic laws covering their interface. This makes interoperation easier as the interface and its properties are given. They are also a lot more general, in my experience, than OO patterns. Monads are famously general---so difficult to pin down that many people, including me at one time, struggle to see the point. This gives them great power, though. Finally, FP patterns like monads are just about unusable without a (modern) static type system. I should know---I implemented a monadic library in Racket and debugging it was a total nightmare. I would find it easier now that I am more experienced with such things, but I believe the clarity enforced by the type checker was critical to building the mental model I now use. This clarity of "thinking in types" is something I started to develop while using Racket, and I found as I went down that route more and more of my code became easily typeable with a classic ML style type system. I came to see a lot of my old code as rather goofy and ill thought out. So this gets to what may the point (but I'm not sure; I'm kicking this from my head). Python, Ruby, and friends are culturally old languages. They were formed in a time (early 90s) when getting hold of PL research was hard. The look back to the OO languages of the 80s for inspiration, for the most part. It's also the case that statically typed FP wasn't really viable till about 2005 or so. That's when Scala came on the scene, and Haskell started to get enough libraries to make it usable. Also the techniques used in modern statically typed FP are surprisingly new. "The Essence of the Iterator Pattern" is 2009, for example, and techniques for monad composition is still an active area of research. I think we're really seeing a cultural shift. I'm old enough to remember when OO was the new hotness. Java being fully OO was a big deal in 1997 when I first heard about it. The primarily OO languages now feel to me like they are the past. As FP knowledge becomes more widespread (and particularly as CS students graduate having learned about it) it's beginning to take the place of OO. When more people understand, say, algebraic data types I think we'll see less need for gradual typing. More people will have the mental model of statically typed FP and write code that doesn't need dynamic typing. On the flip side I don't know that a language community like Python's can ever entirely transition to a new paradigm. Finally, I don't think FP is a silver bullet, though it does bring genuinely new and useful stuff to the table. Nor will we all switch to Haskell. It's the nature of the industry to build on the past, which is why languages like Scala with a strong backwards-compatibility story are successful. We're certain to take something from OO into the future, but I expect we'll be seeing more from statically typed FP and I'm not sure where gradual typing will find its home here. <WALL OF TEXT OVER. THANKS FOR READING!>
TazeTSchnitzel 11y ago
It's interesting that "sound gradual typing" (i.e. static analysis with runtime type checks, AIUI) has supposedly caused large performance problems in some languages. Hack, Facebook's sound, gradually-typed dialect of PHP, doesn't seem to have this problem. And PHP itself, which doesn't do any static type checks itself (you must use a separate static analyser if you want that), only runtime ones, has had limited type checking for eleven years, without apparent performance problems. Are these systems with performance issues doing something fundamentally different, or more complicated? Perhaps I am misunderstanding something.
- ben_greenman 11y ago
  The systems with performance issues are the sound ones! Hack does not have a type soundness guarantee. The compiler statically checks your type annotations, but then generates untyped PHP code. If Hack-generated PHP interacts with PHP from 5 years ago, "type errors" are possible. (I have to say "type errors" in quotes because a mismatch between originally-typed and originally-untyped PHP could result in any kind of error message, or no error at all!) Systems like Typed Racket do type checking at runtime when interacting with untyped Racket code. These runtime checks are the performance problem, but they do accurately diagnose type errors.
  - TazeTSchnitzel 11y ago
    > The compiler statically checks your type annotations, but then generates untyped PHP code. If Hack-generated PHP interacts with PHP from 5 years ago, "type errors" are possible. That's not entirely true. Though some parts of Hack's annotations are not enforced by the runtime, if you say a function takes an int and pass it a float at runtime, it does throw an error from what I remember. It's correct that Hack doesn't guarantee runtime soundness, though.
jongraehl 11y ago
I prefer mandatory static types + type inference. It is a productivity boost if you're allowed to skip entering type names for local vars. If you ever want to change anything meaningful in a large system, you better have meaningful compile-time checks. The only downside is longer build times, but tools are improving. Outside of legacy projects (Linus loves C! and fantastic library ecosystems for scripting languages) I don't see any future for languages without static typing + inference.
rurban 11y ago
I smell a language problem when the cited problem is only the automatically added boolean checks. Note that scheme (Racket) has explicit #true and #false values, and the type Boolean contains only those, while most other dynamic languages define booleans as nil or null or 0 as false (some even ""), and everything else as true. So you don't have to add type checks for a sound system, only a NULL/nil check, which is done in the op, and does not needed to be added for each argument or return value. So it's only a problem for soundly typed scheme and some other obscure languages with explicit booleans, such as my potion, but not for most other dynamic languages, which have the NULL checks in the op already. Only very few specialized ops which permit no NULL args need this check. I smell a typical Felleisen. He hates types.
rurban 11y ago
I smell a language problem when the cited problem is only the automatically added boolean checks. Note that scheme (Racket) has explicit #true and #false values, and the type Boolean contains only those, while most other dynamic languages define booleans as nil or null or 0 as false (some even ""), and everything else as true. So you don't have to add type checks for a sound system, only a NULL/nil check, which is done in the op, and does not needed to be added for each argument or return value. So it's only a problem for soundly typed scheme and some other obscure languages with explicit booleans, such as my potion, but not for most other dynamic languages, which have the NULL checks in the op already. Only very few specialized ops which permit no NULL args need this check. I smell a typical Felleisen. He hates types.

74 points by bshanks 11y ago

deleted 11y ago

[deleted]

johnbender 11y ago
It's worth noting that this is a peer reviewed conference publication (in POPL no less). So, despite the title a lot of time and thought has gone into the content.

tacos 11y ago

"We find that Typed Racket’s cost of soundness is not tolerable. If applying our method to other gradual type system implementations yields similar results, then sound gradual typing is dead." While some of the data is surprising (22x average slowdown for TypeScript dropping to 6.5% overhead when fully typed) the paper ignores the reason why people kicked and screamed for the functionality to begin with. It had nothing to do with run-time performance. Obviously the tools will improve and you can always strip out the annotations if performance is an issue. Reticulated Python is still an order of magnitude faster than Ruby, so obviously performance doesn't render a technology "dead."

taylorfausak 11y ago
> the paper ignores the reason why people kicked and screamed for the functionality to begin with No it doesn't. The explicitly talk about this in section 7: "The acceptance of Typed Racket in the commercial and open-source Racket community suggests that (some) programmers find a way around the performance bottlenecks of sound gradual typing." > Reticulated Python is still an order of magnitude faster than Ruby Are you suggesting that a slower variant of Python is ten times faster than Ruby? That doesn't match my experience. For what it's worth, Ruby outperforms Python in some benchmarks: http://benchmarksgame.alioth.debian.org/u64q/ruby.html http://benchmarksgame.alioth.debian.org/u64q/ruby.html
- Veedrac 11y ago
  Looking at the first benchmark in the list you gave, just in-lining eval_A in the Python code (as the Ruby code does) makes the Python code competitive with the Ruby. As usual, don't trust the Benchmarks Game; it's not nearly well enough controlled to be a useful data point. (I do agree with your main point, though. CPython ain't that fast.)
  - igouy 11y ago
    As usual, don't trust Joshua Landau: without in-lining eval-A the Ruby code only slows from 102secs to 137secs. As usual, Joshua -- Do the ordinary thing and report specific programs that you think should not be allowed.
    - Veedrac 11y ago
      For those not aware, igouy maintains the Benchmarks Game.
      - igouy 11y ago
        Nothing hidden about that -- http://benchmarksgame.alioth.debian.org/sometimes-people-just-make-up-stuff.html#history http://benchmarksgame.alioth.debian.org/sometimes-people-jus... How to report specific programs that you think should not be allowed -- http://benchmarksgame.alioth.debian.org/play.html#invalid http://benchmarksgame.alioth.debian.org/play.html#invalid
sitkack 11y ago
Are you referring to this paper? http://wphomes.soic.indiana.edu/jsiek/files/2014/08/retic-python-v3.pdf http://wphomes.soic.indiana.edu/jsiek/files/2014/08/retic-py...
- tacos 11y ago
  As referenced in the paper itself, section 6.1.
  - igouy 11y ago
    For those who have not looked at the referenced paper, the last section is -- "6. Conclusions" "…Reticulated programs perform far worse than their unchecked Python implementation…" p10 "Design and Evaluation of Gradual Typing for Python"
    - sitkack 11y ago
      And I would argue that _use-site checking_ is the easiest and obviously the slowest method to attain the stated goal. Python is already slow, this is just going to make things silly. Using the same inference methods as Shedskin [0] along with type annotations, functional tests and property based testing can get both correctness and performance in a gradual layered manner. This paper doesn't prove that gradual typing is broken, it shows that _use-site checking_ happens to be slow for the version of Python that they used (PyPy could very well elide the checks). [0] Shedskin Thesis http://mark.dufour.googlepages.com/shedskin.pdf http://mark.dufour.googlepages.com/shedskin.pdf Iterative Flow Analysis by Plevyak http://plevyak.com/ifa-submit.pdf http://plevyak.com/ifa-submit.pdf Agesen's Cartesian Product http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.88.663&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.88....
      - igouy 11y ago
        My point was simply that there is no section 6.1 in that paper, and what is in the paper does not support `tacos` claim ;-)
deleted 11y ago
[deleted]

kazinator 11y ago

> When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. Assertion without evidence. Lack of static typing is awesome in evolving a system: you can convert a part of it to some new types as "proof of concept" and still load and run the code to get usefully far. You just avoid stepping on the parts which aren't converted/refactored yet. Having something Working Now (tm) is a great motivator for some developers to keep going; it reduces the "activation potential barriers" against creativity. The trick to using dynamic languages is to have a ton of static experience. The typing is in your head, where it doesn't get in the way. What we are seeing a lot of lately is a crop of developers who have never worked in anything but some dynamic language. When I'm working in a dynamic language, my concept of type is consciously coming from all the static experience. That keeps me from doing totally scatter-brained things which are possible. I write code such that most of it could statically check, but with the freedom that some of it doesn't have to. Moreover, I am aware (hopefully!) of which code that is.

vox_mollis 11y ago
Lack of static typing is awesome in evolving a system I really don't follow your logic, here. Few things change more frequently while evolving/hacking together software than the data structures and types. Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems. If anything, it's the evolving/hacking process that's MOST prone to accumulating runtime type errors than any other process.
- kazinator 11y ago
  > Few things change more frequently while evolving/hacking together software than the data structures and types. I tend to agree; it is often correct. (Though sometimes we have solid data structures and types and are able to evolve things without changing them.) Anyway, therefore it follows that if we calcify and ossify data structures and types, we kill the progress, not to mention fun. > Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems. This is blown out of reasonable proportion by static type advocates. In a dynamic system, type is de facto a few bits of value in an object. So the above situation is just another value that is wrong. Static programs also have run-time values that can be wrong. A static program that is supposed to calculate 42 might calculate 43, which has the correct type. To discover the cause, someone will have to sit down and think about the code. Code which has never been exercised by a test case (coverage) should still be regarded as garbage, in spite of passing type checking. It is not known to be correct. Type checked is not the same thing as correct. The graph of "type-value" in typical code is rather trivial. Take any moderately complex algorithm, and ignore what its operations are doing; just consider their input and output types. The resulting graph/tree is a lot simpler than what is going on with the values. Type problems are trivial. That is why it's even possible to move them to compile time and have static languages. Think about it: something that runs for hours or days in order to produce a result (and is not even known to terminate) can be entirely type-checked in a millisecond. We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling. The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking. Or it could sort them in descending order when the expected order is ascending: some test was reversed and the reverse test type checks because the operator is commutative. You still have to either prove your code if possible and feasible, else test it exhaustively if possible, or else test it imperfectly.

noelwelsh 11y ago

I love the work of the PLT group, and wish I had time to give this a better read right now. Barring that, I'll just waffle on related topics. Having worked for about a decade in dynamically typed languages (mostly Racket, with a bit of Ruby and Python) and about the same in modern statically typed languages (mostly Scala, with a bit of O'Caml) I've come to believe that the use of types is more a cultural issue than a technology one at this point in time. Let me attempt to explain. Working in Scala I've come to lean heavily on abstractions like applicatives and monads. When I design systems I now find I naturally break them down into these building blocks. For instance, a stream processing system I've been working on is an applicative functor (though I considered alternate designs that are Kleislis). Error handling is usually a monad. The meaning of the names doesn't matter. The important point I'm building systems by sticking together patterns. The patterns are different to OO design patterns as in the Gang-of-four book, but the core idea is the same. When I was more into dynamic types I didn't lean on patterns so much. I tended to hand design the abstractions in each component, and they didn't always fit together so well as a result. Why the difference? I have a few thoughts. Firstly, I've learned more with time. That's undeniable. But, more importantly, functional patterns have a different feel to OO patterns. They are much more precisely defined, with algebraic laws covering their interface. This makes interoperation easier as the interface and its properties are given. They are also a lot more general, in my experience, than OO patterns. Monads are famously general---so difficult to pin down that many people, including me at one time, struggle to see the point. This gives them great power, though. Finally, FP patterns like monads are just about unusable without a (modern) static type system. I should know---I implemented a monadic library in Racket and debugging it was a total nightmare. I would find it easier now that I am more experienced with such things, but I believe the clarity enforced by the type checker was critical to building the mental model I now use. This clarity of "thinking in types" is something I started to develop while using Racket, and I found as I went down that route more and more of my code became easily typeable with a classic ML style type system. I came to see a lot of my old code as rather goofy and ill thought out. So this gets to what may the point (but I'm not sure; I'm kicking this from my head). Python, Ruby, and friends are culturally old languages. They were formed in a time (early 90s) when getting hold of PL research was hard. The look back to the OO languages of the 80s for inspiration, for the most part. It's also the case that statically typed FP wasn't really viable till about 2005 or so. That's when Scala came on the scene, and Haskell started to get enough libraries to make it usable. Also the techniques used in modern statically typed FP are surprisingly new. "The Essence of the Iterator Pattern" is 2009, for example, and techniques for monad composition is still an active area of research. I think we're really seeing a cultural shift. I'm old enough to remember when OO was the new hotness. Java being fully OO was a big deal in 1997 when I first heard about it. The primarily OO languages now feel to me like they are the past. As FP knowledge becomes more widespread (and particularly as CS students graduate having learned about it) it's beginning to take the place of OO. When more people understand, say, algebraic data types I think we'll see less need for gradual typing. More people will have the mental model of statically typed FP and write code that doesn't need dynamic typing. On the flip side I don't know that a language community like Python's can ever entirely transition to a new paradigm. Finally, I don't think FP is a silver bullet, though it does bring genuinely new and useful stuff to the table. Nor will we all switch to Haskell. It's the nature of the industry to build on the past, which is why languages like Scala with a strong backwards-compatibility story are successful. We're certain to take something from OO into the future, but I expect we'll be seeing more from statically typed FP and I'm not sure where gradual typing will find its home here. <WALL OF TEXT OVER. THANKS FOR READING!>

TazeTSchnitzel 11y ago

It's interesting that "sound gradual typing" (i.e. static analysis with runtime type checks, AIUI) has supposedly caused large performance problems in some languages. Hack, Facebook's sound, gradually-typed dialect of PHP, doesn't seem to have this problem. And PHP itself, which doesn't do any static type checks itself (you must use a separate static analyser if you want that), only runtime ones, has had limited type checking for eleven years, without apparent performance problems. Are these systems with performance issues doing something fundamentally different, or more complicated? Perhaps I am misunderstanding something.

ben_greenman 11y ago
The systems with performance issues are the sound ones! Hack does not have a type soundness guarantee. The compiler statically checks your type annotations, but then generates untyped PHP code. If Hack-generated PHP interacts with PHP from 5 years ago, "type errors" are possible. (I have to say "type errors" in quotes because a mismatch between originally-typed and originally-untyped PHP could result in any kind of error message, or no error at all!) Systems like Typed Racket do type checking at runtime when interacting with untyped Racket code. These runtime checks are the performance problem, but they do accurately diagnose type errors.
- TazeTSchnitzel 11y ago
  > The compiler statically checks your type annotations, but then generates untyped PHP code. If Hack-generated PHP interacts with PHP from 5 years ago, "type errors" are possible. That's not entirely true. Though some parts of Hack's annotations are not enforced by the runtime, if you say a function takes an int and pass it a float at runtime, it does throw an error from what I remember. It's correct that Hack doesn't guarantee runtime soundness, though.

jongraehl 11y ago

I prefer mandatory static types + type inference. It is a productivity boost if you're allowed to skip entering type names for local vars. If you ever want to change anything meaningful in a large system, you better have meaningful compile-time checks. The only downside is longer build times, but tools are improving. Outside of legacy projects (Linus loves C! and fantastic library ecosystems for scripting languages) I don't see any future for languages without static typing + inference.

rurban 11y ago

I smell a language problem when the cited problem is only the automatically added boolean checks. Note that scheme (Racket) has explicit #true and #false values, and the type Boolean contains only those, while most other dynamic languages define booleans as nil or null or 0 as false (some even ""), and everything else as true. So you don't have to add type checks for a sound system, only a NULL/nil check, which is done in the op, and does not needed to be added for each argument or return value. So it's only a problem for soundly typed scheme and some other obscure languages with explicit booleans, such as my potion, but not for most other dynamic languages, which have the NULL checks in the op already. Only very few specialized ops which permit no NULL args need this check. I smell a typical Felleisen. He hates types.

rurban 11y ago