←back to thread

873 points belter | 4 comments | | HN request time: 0s | source
1. cies ◴[] No.42946972[source]
> Gradual, dependently typed languages are the future

I really interested why the author thinks this.

I've seen the general sentiment wrt "the future" go from C to C++ to Java to Ruby to JS (also server-side) and Python.

My own sentiment went from Ruby to Haskell to, well, Kotlin I guess...

I looked into Idris (dependently typed), but did not think it would fit the Overton window[1], to be a reasonable expectation for the future.

1: https://en.wikipedia.org/wiki/Overton_window

replies(2): >>42947202 #>>42949231 #
2. samsartor ◴[] No.42947202[source]
Dependent typing is mainly just that feature of Typescript that `x: number | null` becomes just `x: number` inside an `if (x != null) { ... }` statement.

If you dig deeper into the type theory, it gets really interesting and complicated because types themselves can start to include any arbitrary code. And that's where Idris comes in! But after doing a whole project on Idris in college, I agree it is way outside the overturn window. Python and typescript rightfully keep it simple.

replies(1): >>42947517 #
3. wk_end ◴[] No.42947517[source]
Narrowing, as TypeScript calls it, isn't dependant typing - it's basically just a form of pattern-matching over a sum type.
4. lucasoshiro ◴[] No.42949231[source]
> to C++ to Java to Ruby to JS (also server-side) and Python

I feel that languages are going back to static typing. Newer languages such as Go, Rust, Kotlin, Swift, Dart, Nim etc are all statically typed (I can't remember a language from the last decade that is dynamically typed).

Even some dynamically typed languages are moving towards a more static typed system: for JS we have TS, and for Python we have type hints