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

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.