3 ms·

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

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 4y ago
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 4y ago
  > 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!

dwohnitmok 4y ago

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 4y ago
> 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!