[HN Gopher] Is sound gradual typing dead? Performance problems i...
___________________________________________________________________
Is sound gradual typing dead? Performance problems in Typed Racket
(2016)
Author : fanf2
Score : 38 points
Date : 2025-09-27 14:42 UTC (8 hours ago)
(HTM) web link (dl.acm.org)
(TXT) w3m dump (dl.acm.org)
| the_alchemist wrote:
| Should add (2016)
| zelphirkalt wrote:
| Is there a better link to this? "Enable JavaScript and cookies to
| continue"
| volemo wrote:
| https://dl.acm.org/doi/pdf/10.1145/2837614.2837630
| ashton314 wrote:
| This is called "the dead horse paper" for some reason. There's
| been some interesting work since. This isn't my exact area of
| research, but I'm pretty well versed in it and I work with one of
| the authors on this paper so I'm happy to try and answer any
| questions.
|
| The chief issue here is how do you assign blame to typing
| violations? Typescript is unsound: since it just erases types, an
| untyped library that a typed component is using might return
| something the typed component isn't expecting leading you to get
| a type error in typed code. Gradually typed python variants
| typically are better, though they usually just inspect the shape
| of the data and don't check that eg every element in a list is
| correctly typed as well. This can lead to more unsound behavior.
| Typed Racket is fully sound, but performance can degrade
| spectacularly.
|
| There's been some work reviving the dead horse being beaten in
| this paper. Lmk if you have questions.
|
| More papers:
|
| Muehlboeck, Fabian, and Ross Tate. "Sound Gradual Typing Is
| Nominally Alive and Well." Proceedings of the ACM on Programming
| Languages 1, no. OOPSLA (October 12, 2017): 56:1-56:30.
| https://doi.org/10.1145/3133880.
|
| Moy, Cameron, Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van
| Horn. "Corpse Reviver: Sound and Efficient Gradual Typing via
| Contract Verification." Proceedings of the ACM on Programming
| Languages 5, no. POPL (January 4, 2021): 53:1-53:28.
| https://doi.org/10.1145/3434334.
|
| Lazarek, Lukas, Ben Greenman, Matthias Felleisen, and Christos
| Dimoulas. "How to Evaluate Blame for Gradual Types." Proceedings
| of the ACM on Programming Languages 5, no. ICFP (August 18,
| 2021): 68:1-68:29. https://doi.org/10.1145/3473573.
| mirekrusin wrote:
| Type erasure has nothing to do with soundness - ocaml also
| erases types at runtime but it is sound. In typescript "any"
| type, unsafe casting, non null assertions and couple of other
| constructs are unsound. Gradual typing at package level was
| addressed by (also unsound) declaration repository (overall
| successful I'd say - primary reason it won over flow in my
| opinion).
|
| I have a problem reconciling "sound gradual typing" - is there
| such thing at all? Sounds like contradiction to me, no? Untyped
| function's result can be considered "unknown" (as opposed to
| "any" using typescript terminology) and require runtime checks
| at call site (as if it was i/o boundary) - that's fine but
| arguments on the other hand must have some type declaration on
| its signature to be considered sound. Injecting runtime checks
| in untyped library for arguments feels nonsensical because if
| you can do it then you already did static code analysis that
| did infer argument types and you can shove it into function
| signature as static type declaration - ie. that's just more
| sophisticated static inference that doesn't require runtime
| code injection.
|
| You could argue that there may be some dynamism that cannot be
| expressed at type level and that requires runtime checks deeper
| in the untyped code but if it cannot be expressed then by
| definition it's unsound and frankly who cares about runtime
| checks nested deeply in untyped code - what's the difference if
| it blows up at runtime in the middle of that untyped function
| with type error or some other error?
| MrJohz wrote:
| > Typescript is unsound: since it just erases types, an untyped
| library that a typed component is using might return something
| the typed component isn't expecting leading you to get a type
| error in typed code. Gradually typed python variants typically
| are better, though they usually just inspect the shape of the
| data and don't check that eg every element in a list is
| correctly typed as well
|
| This is not typically what is meant by soundness. Most gradual
| type systems erase types (see also Python, Ruby, Elixir), and
| provide ways of overriding the type system's inference and
| forcing a certain expression to be typed a certain way, even if
| that type cannot be proven by the type checker.
|
| What makes TypeScript unsound is that, even if you don't
| override the type checker at all, there are certain expressions
| and constructs that will produce no compile-time error but will
| produce a runtime error. This is a deliberate choice by the
| TypeScript team to make the type checker less correct, but
| simpler to use and adopt. The Flow type checker took the
| opposite approach and was sound, but was occasionally harder to
| use.
|
| I believe most type checkers in other languages tend to hew
| closer to the TypeScript approach, and favour being intuitive
| to use over being completely sound. However, they do work in
| the same way of being compile-time constructs only, and not
| affecting runtime at all. Python is slightly exceptional here
| in that the type annotations are available as metadata at
| runtime, but are not used for type checking unless the user
| explicitly checks them at runtime. There are a couple of
| runtime libraries that add decorators that automatically do
| this runtime type checking, but (a) their usage is fairly rare,
| and (b) their presence does not change how the type checker
| behaves at all.
| bolangi wrote:
| Gradual typing seems to be alive in the Raku language. I can't
| comment on soundness guarantees.
___________________________________________________________________
(page generated 2025-09-27 23:01 UTC)