> Language-level support for sum types doesn't change that; programs written in Scala carry just as much risk of nontermination as programs written in Scala-wit

> Language-level support for sum types doesn't change that; programs written in Scala carry just as much risk of nontermination as programs written in Scala-without-pattern-matches. Admitting nonterminating computations is actually a good thing. What's a bad thing is conflating computations with the values they produce. In other words, the types `Bool` and `ChurchBool` are not isomorphic. > I'm not talking about having runtime checks for things that are statically knowable, I'm talking about runtime checks for things that aren't statically knowable like the size of an array received from an external source. Again, how is that any different from what you would do in a language with "true" dependent types? There's no difference here. But you totally glossed over my point that your abstract type of arrays with a member type of indices would have to be bloated with every operation imaginable on indices.