[dwohnitmok]

Without dependent types you can't do your common constraints in an order independent way.

You end up with four choices:

1. Have a single function that does all the constraint checking at once

2. Have a single linear order where each constraint check feeds into the next but only in that order

3. Acquiesce to a combinatorial explosion of functions that check every possible combination of those constraints

4. Give up keeping track of the constraints at a type level.

[Quekid5]

I do think you can... just via phantom type parameters and type-level programming. In Scala you'd probably use Refined.

(But I'm not expert, admittedly, and I 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.)

[dwohnitmok]

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.

[Quekid5]

> I think this is only true because there isn't a production-ready dependently typed language [...]

Now this I definitely agree with. I want to see what's possible!