←back to thread

Software development topics I've changed my mind on

(chriskiehl.com)
873 points belter | 2 comments | 05 Feb 25 09:50 UTC | HN request time: 0.432s | source
Show context
cies ◴[05 Feb 25 11:21 UTC] 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 #
1. samsartor ◴[05 Feb 25 11:48 UTC] 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 #
2. wk_end ◴[05 Feb 25 12:25 UTC] 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.