3 ms·
Yes, this is called refinement typing (which is a special case of dependent typing). Idris and Agda are probably the dependently typed languages that are closes
by consilient 4y ago
Yes, this is called refinement typing (which is a special case of dependent typing). Idris and Agda are probably the dependently typed languages that are closest to being usable for general purpose programming, but they've still got a ways to go.