I have come back after about 6 months, and I appreciate the relatively informal nature of your blog post on HM type systems. I have since learned much more about intuitionistic type theory, the formalized algorithm for HM inference, and translations of such formalized algorithms into set operations on Maps (write you a Haskell has a chapter that really helps understanding that).
Anyway, I am itching to write another ML toy compiler that the world doesn’t need, because why wouldn’t I do that with this knowledge to ensure I keep it 🙂 Anyway, when I first read this post it was a bit over my head. This time around it is very clear, and seeing the product of my learning quantified in such a way is invigorating. Thank you for your article, and thank you for helping me have the confidence to work with type theory!
I have come back after about 6 months, and I appreciate the relatively informal nature of your blog post on HM type systems. I have since learned much more about intuitionistic type theory, the formalized algorithm for HM inference, and translations of such formalized algorithms into set operations on Maps (write you a Haskell has a chapter that really helps understanding that).
Anyway, I am itching to write another ML toy compiler that the world doesn’t need, because why wouldn’t I do that with this knowledge to ensure I keep it 🙂 Anyway, when I first read this post it was a bit over my head. This time around it is very clear, and seeing the product of my learning quantified in such a way is invigorating. Thank you for your article, and thank you for helping me have the confidence to work with type theory!