Система F

Обогатил ру-Википедию стать ей про это дело. Ловите. Надо бы ещё, конечно, понаписать про точное определение и всякие свойства, но пока лень.

UPD: Понаписал про формальности.

UPD2: Добавил типизацию по Карри с классическим примером, демонстрирующим, что System F богаче просто-типа-лямбды. И готовящим читателя к рассуждениям про импредикативность и ограниченные версии System F.

UPD3: Уф. Доделал-таки.