Dependent typing is mainly just that feature of Typescript that `x: number | null` becomes just `x: number` inside an `if (x != null) { ... }` statement. If yo

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.