Hacker News new | ask | show | jobs
by kbr 2051 days ago
I think you might be describing refinement type systems [1]?

[1] https://en.wikipedia.org/wiki/Refinement_type

1 comments

I've been reading about that, can't seem to wrap my head around the difference between refinement and dependent types.
I 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.