You can't with phantom type parameters and type-level programming alone, although you can get close. Scala's and Haskell's Refined both don't let you do what I'm thinking of.
You can get very close with type-level sets although at this point compile times probably go through the roof. You're basically emulating row types at this point.
def wrapIntoRefined(str: String): Refined[String, Unit]
def validate0[A](str: Refined[String, A]): Either[Error, Refined[String, And[Condition0, A]]]
def validate1[A](str: Refined[String, A]): Either[Error, Refined[String, And[Condition1, A]]]
// This requires ordering Condition0 before Condition1 but if we resorted
// to a type-level set we could get around that problem
def process(input: Refined[String, And[Condition1, And[Condition0, Unit]]]): Unit
// But linearity is still required in some sense. We can't e.g. do our checks
// in a parallel fashion. You still need to pipe one function right after another
The central problem is if you have two validation functions
if you try to recombine them downstream, you don't know that `Refined[String, Condition0]` and `Refined[String, Condition1]` actually refer to the same underlying `String`. They could be refined on two completely separate strings. To tie them to a single runtime String requires dependent types.
You can approximate this in Scala with path-dependent types, but it's very brittle and breaks in all sorts of ways.
> isn't an actual problem of much consequence in practical programming in Haskell or Scala. Opaque types do the 80% bit of 80-20 just fine.
I think this is only true because there isn't a production-ready dependently typed language to show how to use these patterns effectively. In much the same way that "parse don't validate" isn't really much of a problem of consequence in older style Java code because sum types aren't really a thing, if there was an ergonomic way of taking advantage of it, I firmly believe these sorts of dependently typed tagged types would show up all over the place.
You can get very close with type-level sets although at this point compile times probably go through the roof. You're basically emulating row types at this point.
The central problem is if you have two validation functions if you try to recombine them downstream, you don't know that `Refined[String, Condition0]` and `Refined[String, Condition1]` actually refer to the same underlying `String`. They could be refined on two completely separate strings. To tie them to a single runtime String requires dependent types.You can approximate this in Scala with path-dependent types, but it's very brittle and breaks in all sorts of ways.
> isn't an actual problem of much consequence in practical programming in Haskell or Scala. Opaque types do the 80% bit of 80-20 just fine.
I think this is only true because there isn't a production-ready dependently typed language to show how to use these patterns effectively. In much the same way that "parse don't validate" isn't really much of a problem of consequence in older style Java code because sum types aren't really a thing, if there was an ergonomic way of taking advantage of it, I firmly believe these sorts of dependently typed tagged types would show up all over the place.