This is nice and genuinely entertaining https://youtu.be/IOiZatlZtGU https://youtu.be/IOiZatlZtGU (Propositions as types by phil wadler). Its true focus is the

This is nice and genuinely entertaining https://youtu.be/IOiZatlZtGU https://youtu.be/IOiZatlZtGU (Propositions as types by phil wadler). Its true focus is the 1-1 mapping between type systems and logic systems, but it's well worth the watch. This is good reading - it demystifies the funny typing rules in their mathematical form. https://legacy-blog.akgupta.ca/blog/2013/05/14/so-you-still-dont-understand-hindley-milner/ https://legacy-blog.akgupta.ca/blog/2013/05/14/so-you-still-... (Neither of these tell you how to implement the checker yourself though)