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.