[nv-vn]

Yes. They're amazing for theorem proving (see Agda, Idris). They're also useful for refinement types, proving type class laws like for monads, etc.

[alkonaut]

Is there a hello world-y example of refinement types, similar to Vectors with length?