|
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 def validate0(str: String): Refined[String, Condition0]
def validate1(str: String): Refined[String, Condition1]
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. |
Now this I definitely agree with. I want to see what's possible!