Extending ML with semiexplicit higher-order polymorphism

Abstract. We propose a modest conservative extension to ML that al-lows semi-explicit higher-order polymorphism while preserving the essen-tial properties of ML. In our proposal, the introduction of polymorphic types remains fully explicit, that is, both the introduction and the exact polymorphic type must be specied. However, the elimination of poly-morphic types is now semi-implicit: only the elimination itself must be speci ed as the polymorphic type is inferred. This extension is particu-larly useful in Objective ML where polymorphism replaces subtyping