4 ms·
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.
by nv-vn 9y ago
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 9y agoIs there a hello world-y example of refinement types, similar to Vectors with length?