Vérification de type et reconstruction: équations et unification

Cette séance de cours couvre les concepts de vérification de type et de reconstruction de type dans le calcul lambda, en se concentrant sur la transformation des jugements en équations et en utilisant l'unification pour trouver des solutions de type. Il explore également la solidité et l'exhaustivité des systèmes de types, le système Hindley / Milner, le polymorphisme et la traduction des programmes dans le système F. L'instructeur explique les limites de Hindley / Milner, l'essence des expressions let et l'importance des principaux types dans les schémas de types.