3 ms·
I think you might be describing refinement type systems [1]? [1] https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type
by kbr 6y ago
I think you might be describing refinement type systems [1]?
[1] https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type
- kylereeve 6y agoI've been reading about that, can't seem to wrap my head around the difference between refinement and dependent types.
- kbr 6y agoI think dependent types are stronger than refinement types because they can encode types that don't necessarily have to be decidable. Refinement types are used for creating subsets of a type, while dependent types can be used for creating arbitrary types based on values. As a result, dependent types are more powerful, but they might be too much if all you need are some constraints on an existing type.