Невозможно понять термин F-омега

Я читаю статью о Fω и не могу понять причины этого утверждения:

Типовой член типа (∀γ:*. F γ → β) показывает, что F - постоянная функция, которая всегда возвращает β.

Я предполагаю, что "F γ → β" - это термин типа, т. Е. Тип стрелки. Этот тип стрелки является типом функции, которая принимает аргумент типа, вычисляемый приложением типа "F γ", и возвращает значение типа β.

Если это так, почему F должна быть постоянной (типовой) функцией, которая всегда возвращает β? Разве это не может быть функция произвольного типа, которая возвращает, скажем, α и все еще удовлетворяет проверке типов?

Спасибо за ваше время.

1 ответ

Отвечая на мой собственный вопрос.

Я думаю, что причина в параметричности.

Если бы "F γ" мог возвращать любой тип, например α, функция (тип которой передается с помощью типа ∀) имела бы тип α → β.

Параметричность диктует, что все экземпляры этой полиморфной функции должны иметь одинаковое поведение, что возможно только в том случае, если это единичная функция, т. Е. Типа β → β, поэтому подразумевается, что "F γ" всегда возвращает β.

Другие вопросы по тегам