|Playlist||schedule page slides as PDF|
Extending our language to support parametric polymorphism.
Examples for interp and typecheck for LAMBDA and @. The interp additions are simple enough that we say no more about them; see poly-lambda.rkt.
Polymorphism 3 — typecheck (1:57)
Type checking rules for LAMBDA and @. See poly-lambda.rkt.
Polymorphism 4 — datatypes (4:01)
Parameterizing type definitions with respect to a type.
Polymorphism 5 — inference (5:11)
Infering polymorphism and type applications.
Constraining polymorphism to first-order forms (i.e., allowing polymorphic bindings, but not polymorphic values) makes inference simpler and/or more consistent, and it helps explain why plai-typed never shows types with forall.
Looking more at polymorphism works in plai-typed. This information should be helpful for HW 11.
More about plai-typed, specifically polymorophism and define-type. This information also should be helpful for HW 11.
Abtracting functions over a combination of types and other functions. Watch this video only after trying HW 11.