'Missing'(?) feature in programming languages? [duplicate]

Question

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?

Answer 1

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

Answer 2

You can actually mostly define that in Haskell because it's basically an Int plus some semantics. For example, you have to decide what you're going to do with subtractions that go beneath the threshold, like what (-) 6 7 gives. (A common convention with Peano arithmetic is to give 0 -- so in this case it would return 6, the least value of the system.) You also need to choose whether you're going to error on a fromInteger 3 or else whether you're going to store, say, newtype IntGT5 = IntGT5 (Maybe Int) instead of newtype IntGT5 = IntGT5 Int. You have to write all of the typeclass instances yourself, and once you've done that you'll have an appropriate type.

If you've got an abiding interest in this problem, two things to pay attention to are liquid types and subtyping. Let me tell you a little about the latter.

Alan Kay invented OOP to be something different than what it is (he wanted every program to be written as a network of communicating computers), but what it turned out to be in the modern world is basically a way to do complex subtyping. "Duck typing", for example, is about creating an "intersection type" of a bunch of really general types (like `things with a "waddle" method, things with a "quack" method) which other types are subtypes of. So subtyping is very naturally OOP.

The thesis I've linked you to points out another interesting thing about subtyping: you can use subtypes to erase the distinction between type and value. Of course, making types into values does not need subtyping; it is e.g. already the case in the Python language, where you can call type(x) to get an object which represents the type of the object. But the interesting thing is that as subtypes go, you can just define a type 3 :: Int (3 of kind Int) which is the type of all Ints which are equal to 3. It is in essence a unit/void type which is a subtype of a bigger class. By blurring the distinction between 3 of kind Int and 3 of type Int you get every value being a type as well. You could then do something JSON-like with this approach, where {x: Int, y: 3 :: Int} is a type of objects containing two properties x and y where x is any Int and y is the integer 3 :: Int.