Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Thu 27 Aug 2020 12:45 - 13:10 at ML - Session 1

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