Good timing for me! Learning about dependent types has caused a Baader-Meinhof  experience for me–I suddenly see a need for them everywhere!
In particular, TypeScript would benefit tremendously from something approximating dependent types–my own code is already begging for correlated record types and there are numerous related GitHub issues:
Obviously, this is a difficult thing to implement and could make type checking quite a bit more expensive. But if anyone can do it, it’s certainly the TypeScript team that can!
 I always assumed Baader and Meinhof were famous psychologists, but apparently it refers to a militant West German terrorist group! Thankfully, Streisand is a musician.
Excellent, thanks a lot for post! There’s a lot of fun with dependent types, so I’m looking forward to read the paper.