If you want to see a dependently typed (technically, though the term often doesn't include this class of languages in practice) language which enforces smaller sets of properties more eloquently take a look at Liquid Haskell
The core idea here is called the Refinement Type which is basically what you're looking for. In order to power this type system Liquid Haskell depends on a full SMT solver, though, which is a rather large hammer to wield.
As it regards to Peano arithmetic in DT languages the Peano naturals data type is awkward for doing math... but FANTASTIC for defining the properties of recursion and induction. Indeed, what you find is that the Peano nats show up everywhere as being a stable foundation for complex proofs and smart recursive functions.
It's a very similar feature to Haskell's lists. Competent Haskell programers do not use lists when they want arrays or vectors—the latter types are naturally far more convenient when in their application space. But lists are not abolished! They're fantastically useful as control structures indicating sequential recursion.
Typically you think of data types as forming their meaning through construction. You use numbers by constructing them according to arithmetic properties. Another way to do it, though, especially with recursive ADTs and inductive families, is to think of a type's meaning as being derived from how you break it down.
The canonical way to break down a list is to find some way of combining the head of the list with the broken-down version of the tail of the list. In Haskell that is called foldr
-- combiner zero list result
foldr :: (a -> b -> b) -> b -> [a] -> b
and you can see its canonicity by thinking of it as simply replacing the constructors for a list by the arguments to foldr.
let ls = Cons 1 (Cons 2 (Cons 3 Nil)))
foldr comb zero ls =
comb 1 (comb 2 (comb 3 zero)))
http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/
The core idea here is called the Refinement Type which is basically what you're looking for. In order to power this type system Liquid Haskell depends on a full SMT solver, though, which is a rather large hammer to wield.
As it regards to Peano arithmetic in DT languages the Peano naturals data type is awkward for doing math... but FANTASTIC for defining the properties of recursion and induction. Indeed, what you find is that the Peano nats show up everywhere as being a stable foundation for complex proofs and smart recursive functions.
It's a very similar feature to Haskell's lists. Competent Haskell programers do not use lists when they want arrays or vectors—the latter types are naturally far more convenient when in their application space. But lists are not abolished! They're fantastically useful as control structures indicating sequential recursion.
Typically you think of data types as forming their meaning through construction. You use numbers by constructing them according to arithmetic properties. Another way to do it, though, especially with recursive ADTs and inductive families, is to think of a type's meaning as being derived from how you break it down.
The canonical way to break down a list is to find some way of combining the head of the list with the broken-down version of the tail of the list. In Haskell that is called foldr
and you can see its canonicity by thinking of it as simply replacing the constructors for a list by the arguments to foldr.