Am 09.02.2016 um 18:04 schrieb Carter Schonwald:
I'd like to opine that I personally like that our types are getting more honest in reflecting how things work,
I'm pretty much in the same boat with that. I just have a feeling that the typing is getting complicated because the compiler isn't good enough to infer whether a type is lifted or not, boxed or not. Essentially, there's that constant temptation to give programmers access to machine integers. It's a valid concern, but it complicates the type system tremendously. I feel that this is similar to expressing value constraints in the type system, e.g. ranges or squareness of matrixes. Yes it can be done in Haskell's type system, yes it does typecheck beautifully, but the type declarations behind these kinds of feats will just make any ordinary programmer go MEGO. Even the bright ones. I conclude that the type system isn't the right place for that kind of checking. To be understandable, such constraints need to be expressed as boolean assertions, not as some inductive construct. YMMV.