Hmm, I think you can do that too, but you'd have to assign each int value its own singleton type, which would be ridiculous and not gain you anything since you're just moving the logic up one level in the hierarchy of universes.
> what people mean when they talk about programming in types
If the type system is powerful enough then you can express any function at the type level. Some languages with universal polymorphism make no difference between types and terms. Any function can also be used at the type-level, kind-level and so on. Though usually just defining a simple wrapper type with smart constructor will get you 80% of the way in a business application with 2% of the effort of real type-level programming.
Hmm, I think you can do that too, but you'd have to assign each int value its own singleton type, which would be ridiculous and not gain you anything since you're just moving the logic up one level in the hierarchy of universes.
> what people mean when they talk about programming in types
If the type system is powerful enough then you can express any function at the type level. Some languages with universal polymorphism make no difference between types and terms. Any function can also be used at the type-level, kind-level and so on. Though usually just defining a simple wrapper type with smart constructor will get you 80% of the way in a business application with 2% of the effort of real type-level programming.