PL basics

There is a problem with mixing impredicative polymorphism, i.e., polymorphism in System F, and side effects, e.g., references, continuations, etc. This problem arises when we allow arbitrary computations to considered polymorphic. The solution usually used is to restrict the programming language so that only values are allowed to be abstracted as polymorphic programs. Here we discuss this issue and its solution which is usually referred to as “Value Restriction”.