3 ms·

I meant "practically expressed in their static type systems", ie. in gradual type systems for those languages as currently implemented. Poor wording on my part,

I meant "practically expressed in their static type systems", ie. in gradual type systems for those languages as currently implemented. Poor wording on my part, my bad :) On dependent typing and gradual type systems - I'm not sure they are possible to mix. I think none of the current implementations do anything remotely similar to dependent typing. It would be a really cool if it worked though. I'd love to be able to track length of a list in mypy type system (for example). For the curious: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type https://www.idris-lang.org/pages/example.html https://www.idris-lang.org/pages/example.html

zozbot234 5y ago
Dependent types seem like they would have to be explicitly static, but gradual typing interacts well with "fully static" fragments of your program. (In fact, having entire program modules be statically typed is needed anyway to get proper optimization and reduce the overhead of dynamic checking and conversion.)
- klibertp 5y ago
  > Dependent types seem like they would have to be explicitly static Right, because they lift values into type system, those values need to be well-typed themselves. You wouldn't be able to represent gradually typed dynamic/Any value then, I think. I might be wrong though, my understanding of type theory is limited at best :) > to get proper optimization and reduce the overhead of dynamic checking and conversion That's probably why very few gradual type systems are taken advantage of when optimizing. Typed Racked does this, but Typed Racket disallows untyped values within the typed module. Hack probably does it, too, but I have no experience using it. Common Lisp does it with correct optimization settings. Raku does this, but Raku was written from the ground up with gradual typing in mind. There are projects that try to transpile fully-typed subsets of dynamic languages to C (can't find the link right now), but that's a bit different. Other popular gradual type systems are basically advanced linters. There's a lot of development and potential in this area though, we'll see how it pans out in a few years :)

zozbot234 5y ago

Dependent types seem like they would have to be explicitly static, but gradual typing interacts well with "fully static" fragments of your program. (In fact, having entire program modules be statically typed is needed anyway to get proper optimization and reduce the overhead of dynamic checking and conversion.)

klibertp 5y ago
> Dependent types seem like they would have to be explicitly static Right, because they lift values into type system, those values need to be well-typed themselves. You wouldn't be able to represent gradually typed dynamic/Any value then, I think. I might be wrong though, my understanding of type theory is limited at best :) > to get proper optimization and reduce the overhead of dynamic checking and conversion That's probably why very few gradual type systems are taken advantage of when optimizing. Typed Racked does this, but Typed Racket disallows untyped values within the typed module. Hack probably does it, too, but I have no experience using it. Common Lisp does it with correct optimization settings. Raku does this, but Raku was written from the ground up with gradual typing in mind. There are projects that try to transpile fully-typed subsets of dynamic languages to C (can't find the link right now), but that's a bit different. Other popular gradual type systems are basically advanced linters. There's a lot of development and potential in this area though, we'll see how it pans out in a few years :)