Something like this could be implemented in Haskell or OCaml using GADTs[0]. You can add a phantom type parameter to the expression type and use that indicate whether or not the expression is well-formed according to some predicate--in your example, "non-nested added-ness." In fact this technique is often used as an introductory example to the use of GADTs, except the well-formed-ness property that's typically presented is that the expression is well-typed.
It's possible to express multiple properties using the same phantom type parameter is both languages. However, as you sort of alluded to, this encoding is much simpler if your language supports subtyping. Since OCaml does support subtyping, you can use polymorphic variants[1] for this purpose. For example, if you had the NotAdd property as well as the NotMult property, you could write down the type for an operation that depends on just the NotAdd operation like this:
val notAddOp : ([> `NotAdd] as 'a) expr -> 'a t
... and write down an operation that depends on both like this:
val bothOp : ([> `NotAdd | `NotMult] as 'a) expr -> 'a u
In Haskell, things would get more complicated. The type of the first operation would like more like this:
notAddOp : Contains NotAdd a -> Expr a -> T a
... where the first argument is acting like a proof witness that the type parameter 'a in some sense "contains" tye type NotAdd. Similarly again for the second, except with two witnesses:
bothOp : Contains NotAdd a -> Contains NotMult a -> Expr a -> T a
I haven't thought it completely through, but I'm almost certain that a combination of type classes and GCH extensions would allow you to turn those proof witness arguments into type class contexts.
Anyways, doing this sort of encoding of properties in types is all well and good until you start considering more realistic examples. Even in the one you presented, it's going to cause you problems if, say, you want to write an inliner for your language. Substituting an expression for a variable within a "NotAdd" addition may very well break the "NotAdd" property. This means that your inliner has to be aware of that property, so that it can preserve it while doing its job. In other words, the option of writing code that will break an invariant, and then immediately recover the invariant, is no longer on the table when you take this approach to verifying the correctness of your code. That may seem bad, until you try to verifiably balanced red-black tree without learning Coq and reading this[2].
An inliner might break NotAdd, but why would it need to preserve it? Presumably an inliner is meant to be a homomorphism, not an isomorphism - i.e., it only goes one way.
Also, FreeBool[A] (the example given) actually handles substitution quite well. The `flatMap` operation will properly flatten things out:
If you're not careful about how you encode a property, the type system will _require_ you to preserve that property throughout each step of the computation, regardless of what sort of morphism that computation is. (It's an endomorphism.) Now that may be simple and straightforward when dealing with structural recursion over a boolean language, but if you want to write an inliner for Haskell, for example, it's probably a better idea to drop invariants from types (but not from the computation, of course), run the algorithm, and reintroduce invariants to the types afterwards.
Again, that example's way overshooting the complexity needed to prove the point. Even a seemingly simple invariant like the red-black balancing property is one that is impractical to preserve in this fashion without a proof assistant. And even then its practicality is still dubious.
It's possible to express multiple properties using the same phantom type parameter is both languages. However, as you sort of alluded to, this encoding is much simpler if your language supports subtyping. Since OCaml does support subtyping, you can use polymorphic variants[1] for this purpose. For example, if you had the NotAdd property as well as the NotMult property, you could write down the type for an operation that depends on just the NotAdd operation like this:
... and write down an operation that depends on both like this: In Haskell, things would get more complicated. The type of the first operation would like more like this: ... where the first argument is acting like a proof witness that the type parameter 'a in some sense "contains" tye type NotAdd. Similarly again for the second, except with two witnesses: I haven't thought it completely through, but I'm almost certain that a combination of type classes and GCH extensions would allow you to turn those proof witness arguments into type class contexts.Anyways, doing this sort of encoding of properties in types is all well and good until you start considering more realistic examples. Even in the one you presented, it's going to cause you problems if, say, you want to write an inliner for your language. Substituting an expression for a variable within a "NotAdd" addition may very well break the "NotAdd" property. This means that your inliner has to be aware of that property, so that it can preserve it while doing its job. In other words, the option of writing code that will break an invariant, and then immediately recover the invariant, is no longer on the table when you take this approach to verifying the correctness of your code. That may seem bad, until you try to verifiably balanced red-black tree without learning Coq and reading this[2].
Life's full of trade-offs.
[0]: https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ...
[1]: https://realworldocaml.org/v1/en/html/variants.html#polymorp...
[2]: http://www.cs.princeton.edu/~appel/papers/redblack.pdf