Semi-explicit first-class polymorphism for ML

We propose a modest conservative extension to ML that allows semi-explicit first-class polymorphism while preserving the essential properties of type inference. In our proposal, the introduction of polymorphic types is fully explicit, that is, both introduction points and exact polymorphic types are to be specified. However, the elimination of polymorphic types is semi-imp licit: only elimination points are to be specified as polymorphic types the mselves are inferred. This extension is particularly useful in objective ML where polymorphism replaces subtyping. (C) 1999 Academic Press.