В Системе F тип exists a. P может быть закодирован как forall b. (forall a. P -> b) -> b в том смысле, что любой термин Системы F, использующий экзистенциал, может быть выражен в терминах этого кодирования с соблюдением правил набора и сокращения.
В разделе «Типы и языки программирования» появляется следующее упражнение:
Можем ли мы кодировать универсальные типы в терминах экзистенциальных типов?
Моя интуиция говорит, что это невозможно, поскольку в некотором смысле механизм «экзистенциальной упаковки» просто не так мощен, как механизм «абстрагирования типа». Как мне официально показать это?
Я даже не уверен, что мне нужно доказать, чтобы формально показать этот результат.