Search code examples
haskelltypeslanguage-designtype-systems

'Missing'(?) feature in programming languages?


Let's take Haskell as an example, as it gets the closest to what I'm about to describe of the languages I know.

A type, Int for example, can be viewed as the set of all possible values (of that type). Why is it that we only get to work with very specific sets? Int, Double, etc... and not with all their subsets in the type system.

I would love a language where we can define arbitrary types like Int greater than 5. Are there examples of such languages? If not, why not?


Solution

  • You are looking for Dependent types. Idris, Agda and Coq are well known in this category.