The usual declarative presentation of ML allows implicit generalisation and instantiation anywhere in a program. We consider a mild variant, Explicit ML, with explicit syntax for generalisation and instantiation. The familiar implicit ML syntax may be recovered by way of syntactic sugar for variables and let-bindings.
FreezeML is a small extension of ML providing first-class polymorphism and sound and complete type inference of principal types, whose typing rules are not declarative.
We show that Explicit ML extends naturally to Explicit FreezeML, a declarative presentation of an explicit variant of FreezeML. The familiar implicit FreezeML syntax may be recovered by way of syntactic sugar. Explicit FreezeML is a conservative extension of both Explicit ML and System F.
The Virtues of Semi-Explicit Polymorphism (ml2020-final91.pdf) | 609KiB |
Thu 27 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
11:30 - 11:55 Talk | Tracking injectivity and nominality beyond abstraction ML Jacques GarrigueNagoya University Media Attached File Attached | ||
11:55 - 12:20 Talk | Quantified Applicatives – API design for type-inference constraints ML Media Attached File Attached | ||
12:20 - 12:45 Talk | High-level error messages for modules through diffing ML Media Attached File Attached | ||
12:45 - 13:10 Talk | The Virtues of Semi-Explicit Polymorphism ML Frank EmrichUniversity of Edinburgh, UK, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, Jan StolarekUniversity of Edinburgh, UK Media Attached File Attached |