No responses yet - I get the feeling that no-one “owns” the documentation.
Maybe it’s not (only) about what is possible with more advanced type systems but whether these type systems are easily available in their context.
That said, I have no idea how much work it is to support more advanced type systems compared to “simpler” type systems. :smile:
Using dependent types today means Coq/Adgda/Idris (maybe Haskell?), right? Some of those are ruled out immediately (Coq doesn’t permit infinite loops!), and others might be a big enough hurdle that it’s really not worth it?
I mean, Typed Racket has dependent types…
Til :scream:
Also, it turns out that you can write all the interesting programs you want without infinite loops, assuming that your language includes codata (which both Agda and Coq do).
I mean in Typed Racket you can do, like, > (ann 42 (Refine [n : Integer] (< n 43)))
- : Integer [more precisely: (Refine (x₀ : Integer) (<= (+ 1 x₀) 43))]
42 which isn’t quite dependent types (although TR has those too)
also see http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=FEB09646F4C1F44349051B570A1A0567?doi=10.1.1.22.2636&rep=rep1&type=pdf for an example of simulating dependent types in Haskell, or at least simulating what dependent types can do
there’s a lot you can do with type-level programming without having dependent types
My comment was more about how they seemed to assert that static typing couldn’t ever handle constraining a number to within a certain range - or, at least, that’s how it read to me ¯_(ツ)_/¯
I read « static typing in langs web devs are familiar with » (which is like, Java ? Typescript? C#? Python/Ruby ?)