But note that achieving the strictness type requires the use of `seq` which is perhaps, arguably, a more arbitrary language feature than function abstraction and unit are! In particular, it's been a big debate as to what the proper semantics for seq are—the dust is technically unsettled, despite the long history of seq in Haskell.

And w.r.t. to monads, for a lot of people it is! Most use of monads is done implicitly, right? ;) The only reason Haskellers tolerate the extra syntax is because it's statically required (I claim).

There's an advantage here, of course, in statically ensuring that people do something more explicitly than they would like to. Perhaps the same advantage applies to thunking.

Honestly, I'd rather not comment. I don't know that I or nearly anyone has enough information to make strong, confident opinions about the "right way" to do lazy/strict. I'm hoping that the research into total languages will provide answers!