I think it's tragic how easily dismissed ML/Miranda-evolved languages are considered a priori bad. What is more interesting about a sound type system is what c

I think it's tragic how easily dismissed ML/Miranda-evolved languages are considered a priori bad. What is more interesting about a sound type system is what category theory enables. Proven composition, sound abstractions, etc. I'm not a huge fan of category theory but it undeniably useful. In practice this means we get very rich, provable composition. It's quite liberating how far good, reasonable constraints can take you.