[dwohnitmok]

> And as you write more and more code you have exponentially more type parameters, because you have no way to just evaluate functions of type parameters, so you have to pass markers that represent all of your type relationships right from the initial input part of your program all the way down

This isn't really the thing that dependent types provide though. If you have type-level computation without dependent types that's enough to avoid this problem (and e.g. Scala has this). However, dependent types are when the `+` in your first append is the same `+` as the usual runtime `+` rather than a separate type-level function that only works with types, not runtime values. Scala does not have this. Its dependent types are much more limited.