Cool but useless example of typelevel-valuelevel equivalence

typelevel_valuelevel.scala

// Type Level
type U[M[_]] = M[Int]
type Bi[A, B] = Map[A, B]
type X[A] = U[[A] =>> Bi[String, A]]
implicitly[X[Int] =:= Bi[String,Int]]
// Result: =:=[X[Int], Map[String, Int]]
// Note that this is also true: implicitly[X[java.util.Date] =:= Bi[String,Int]]
// hence this example is not very good

// Value level
case class Blah(v: String)
val intBlah = Blah("123")
val stringBlah = Blah("Joe")
val dateBlah = Blah("1943")

val u = (m: Blah => Blah) => m(intBlah)
val bi = (a: Blah, b: Blah) => Blah((a, b).toString)
val x = (a: Blah) => u((b: Blah) => bi(stringBlah, b))
x(intBlah) == bi(stringBlah, intBlah)
// x(dateBlah) == bi(stringBlah, intBlah)
// This also works, hence the example isn't very good
// Result: true

I don't have a twitter account so I thought I'd ask here if you don't mind. If you think this is the value level equivalent of the left side of the image you posted then why didn't you post this on the right side? It feels like you are comparing apples to oranges just to prove a point(which might be true but this is certainly not a proof of that). Or why didn't you post the type level equivalent of the right side of your image? Something like this:

sealed trait Nested
sealed trait Outer[N <: Nested] extends Nested
sealed trait Inner[N <: Int] extends Nested

type Core[N <: Nested] = N match
  case Outer[n] => Core[n]
  case Inner[n] => n

summon[Core[Outer[Outer[Inner[123]]]] =:= 123]

It doesn't look so bad, does it?

Or we could also replace the right-hand side with the value-level of the left hand side:

val u = (m: Blah => Blah) => m(intBlah)
val bi = (a: Blah, b: Blah) => Blah((a, b).toString)
val x = (a: Blah) => u((b: Blah) => bi(stringBlah, b))
x(intBlah) == bi(stringBlah, intBlah)

Would that make anything better?

@erdeszt You sound like a reasonable person so I'll try to respond as reasonably as I can. The point of my post was not to compare an equivalent type-level and value-level technique. It was a comment on the kinds of common techniques found in type-level and value-level computation in a general sense. Match-types certainly simplify computations on nested typelevel-structures such as the example you presented, however, aside from operations on highly advanced record types (a use-case which is largely subsumed by Dotty's Tuple type), there are very few cases of match-types being used as far as I know. What is far, far more common on the type-level is the necessity of various kinds of reduction on complex effect types in order to support unification of single, stream, resource and other effect types. Also, type-level reductions are frequently used in libraries that support advanced encoders via typeclasses that (in many cases) take advantage of multiple generic parameters, underscores, and phantom-types in order to drive control-flow. In all of these cases, the most important thing is to understand how types are reduced. Without that knowledge, these libraries are inscrutable.

Free-grammar value-level techniques on the other hand, can typically be used avoid the need for highly-complex abstract effect types (i.e. various forms of F[_] with 3 or more holes) and typeclasses, hence they remove the need for type-level techniques (in many, many cases). Value-level control flow in free grammars does not require the use of additional type-parameters with their inherent requirement of underscores and phantom-types. Thus, in a general sense, free-grammers reduce the need for overly complex type-level logic because they eliminate the need for abstract effect-types and typeclasses that require this type-level logic in the first place.

A more flushed-out version of my argument would go roughly along the lines of "if you don't use free grammars, you'll inevitably end up with very complex types and very complex type-level logic that look like jump-kicks." That's not something I could justify in 280 characters but I hope the above two paragraphs give it some credence.

P.S.
You can possibly reduce my argument to "well you're just stuck in 2016 on the whole free-monad craze." That's partially true. Sometimes free-grammars manifest as free-monads and/or free-applicatives but in many cases even simpler structures are possible with a given set of business logic. I wouldn't necessarily argue that all initial encodings are better then final encodings, but I do think that the pendulum has moved into the realm of final-encodings too far.