In turn, the ML family is a deeply depressing thing to see if you've ever been exposed to Idris or Agda.
Quote Tweet
Swift is a deeply depressing thing to see if you've ever been exposed to the ML family. #smlsjNot
4
5
Conversation
Other than a rather dated syntax there is nothing 'depressing' about the ML family. After you write something like MirageOS in Idris or Agda come back and report on the experience 🙃
3
4
“depressing” is an overstatement, but the fact that you can't, say, write a list indexing function without the possibility on every call of it failing makes me sad. (Oh, and Hasochism, or its OCaml equivalent, is actually depressing, so don't suggest that.)
2
3
Dependently typed langs can be disappointing when you learn that you have to duplicate your definitions a bunch and erasure/phase/staging is really hard! 😂
1
2
Oh and effects as well. Super excited about the current work in this area though. I’m hoping I don’t have to be sad about this for too long! 🤞🤞