Anyone know why dependent types aren't a thing in practice? They seem to eliminate a bunch of restrictions induced by phase separation. Easier proving of compile time invariants, seems good.
All the demos I've seen of Idris suggest the compile time cost is substantial. So my best guess at present is the languages take too long to compile but that doesn't seem like it should be a deal breaker.
> Anyone know why dependent types aren't a thing in practice?
Because full dependent types imply no phase separation, as you say. Modern languages like Rust and Zig have introduced more powerful facilities for doing custom things at compile time, and perhaps dependent types can ultimately be viable in the compile-time-only subset of such languages; but we're a long way from dispensing with that phase separation altogether.
All the demos I've seen of Idris suggest the compile time cost is substantial. So my best guess at present is the languages take too long to compile but that doesn't seem like it should be a deal breaker.