There are a bunch of languages like that. I've just done a project in HOL, where all functions must terminate. Proving that functions terminate is a pain in the

There are a bunch of languages like that. I've just done a project in HOL, where all functions must terminate. Proving that functions terminate is a pain in the backside, because for any trivial structurally recursive function you write (easy to prove), there's also a function that's nothing like that and will just be a waste of your time. Also, without a lot of work, you'd get very little out of evaluation models. In particular, the only disadvantage at the moment is that you can't strictly evaluate arguments where the function isn't strict in that argument. That's cases where the argument might not get used. I don't think it would get you massive improvements that you couldn't already get in most cases by simply producing specialised versions of the function. The big advantage is that you can prove more interesting stuff about your code (with again more effort). See Agda, where you can (for example) write a zip function that won't typecheck unless both lists are the same length.