Оператор связывания Haskell в системе F, включая виды

Question

Мне нужно знать, что такое тип System F оператора связывания типа Haskell (>>=).

До сих пор я писал это так:

(M::*->* A::*) -> (A::* -> (M::*->* B::*)) -> (M::*->*  B:*)

Это правильно? Если это правильно, как мне найти окончательный результат?

Спасибо!

Answer 1

Ты почти там. Добавьте явные квантификаторы для переменных типа и удалите аннотации типов при каждом использовании переменной.

∀M:*->*. ∀A:*. ∀B:*. M A -> (A -> M B) -> M B

Я использовал более обычный : вместо Хаскелла ::,

Обратите внимание, что система F не имеет высших видов (например, *->*), поэтому тип выше может быть найден только в более мощных системах типов (например, система Fω).

Кроме того, выше я "удобно" пропустил ограничение класса типов на M, что делает тип близким, но не совсем, типом Haskell >>=, (Также см. Комментарий ниже @DanielWagner).

Эта мелкая деталь важна. В противном случае приведенный выше тип является настолько общим, что он не заселен - ни один лямбда-термин не имеет такого типа. Действительно, предположим, что противоречие есть f имеющий общий тип выше. Затем,

f (λt:*. t->⊥) : ∀A,B:* . (A -> ⊥) -> (A -> B -> ⊥) -> B -> ⊥

где ⊥ - любой пустой тип (например, Voidв Хаскеле). Но тогда, принимая ⊤ быть любого непустого типа (например, ()в Хаскеле с жителем u, мы получаем

f (λt:*. t->⊥) ⊥ : ∀B:* . (⊥ -> ⊥) -> (⊥ -> B -> ⊥) -> B -> ⊥
f (λt:*. t->⊥) ⊥ ⊤ : (⊥ -> ⊥) -> (⊥ -> ⊤ -> ⊥) -> ⊤ -> ⊥
f (λt:*. t->⊥) ⊥ ⊤ (λx:⊥. x) : (⊥ -> ⊤ -> ⊥) -> ⊤ -> ⊥
f (λt:*. t->⊥) ⊥ ⊤ (λx:⊥. x) (λx:⊥. λy:⊤. x) : ⊤ -> ⊥
f (λt:*. t->⊥) ⊥ ⊤ (λx:⊥. x) (λx:⊥. λy:⊤. x) u : ⊥

так ⊥ обитаемо - противоречие.

Более неофициально, вышесказанное просто доказывает, что data T a = T (a -> Void) не может быть монадой.