deniok

В чистой бестиповой лямбде обычное кодирование булевых значений таково

  tru = λt f. t
  fls = λt f. f

При этом условный оператор кодируется так:

  iif = λb x y. b x y

а основные булевы функции так

  not = λb t f. b f t
  and = λa b. a b fls
  or  = λa b. a tru b

Что из этого получится в просто типизированной системе?

Напомним, что просто типизированная лямбда строится следующим образом. Берём за основу бесконечное множество переменных

  Var = {a,b,c,d,...}

Индуктивно определяем, что тип это либо переменная, либо (правоассоциативная) стрелка между типами

  Type = Var | Type -> Type

Затем задаём правила приписывания типов термам - правила вывода типов. Переменной можно приписать любой тип, абстракции - стрелочный

   x:A    M:B
----------------
(λx. M):(A -> B)

Что касается аппликации, то тип левого аппликанда должен быть стрелочным:

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

Здесь метапеременные M и N обозначают произвольные термы, а метапеременные A и B --- произвольные типы.

Вернёмся к типизации булевых термов и функций. Если приписать булевым термам <<простой>> тип, получим

  tru : a -> b -> a
  tru = λt f. t

  fls : a -> b -> b
  fls = λt f. f

Хотелось бы иметь одинаковый тип для истины и лжи, поэтому естественно приписать t и f один и тот же тип (a). Тогда, введя <<сокращение>>

  Bool = a -> a -> a

можем писать желаемые утверждения типизации

  tru : Bool
  fls : Bool

Однако, к сожалению, всё не так просто. Если посмотреть на условный оператор

  iif : Bool -> s -> s -> s
  iif = λb x y. b x y

то возникает такая проблема. Хотелось бы применять iif к значению любого конкретного типа s, но тогда правила вывода дадут

  Bool  = s -> s -> s

Получается, что наш Bool плохо инкапсулирует свои внутренности. Это приводит к проблемам с типизацией. Например, непонятно, какой тип выведется у b в

  problem = λb. pair (iif b 1 2) (iif b "Ann" "Bob")

Есть два выхода.

Выход (1). Расширение просто типизированной лямбды булевыми константами.

(a) ввести константы true, false и iif в термы, как атомы;
(b) ввести константу Bool в типы, как атом;
(c) ввести дополнительные правила типизации true:Bool, false:Bool и схему правил для любого типа s:

  iif : Bool -> s -> s -> s

(d) ввести схему аксиом δ-редукции: для любых типа s и термов x:s и y:s

  iif true  x y  -δ->  x
  iif false x y  -δ->  y

Выход (2). Расширение просто типизированной лямбды до полиморфной лямбды (System F).

  Bool = forall a. a -> a -> a

При таком подходе в терме

  iif = λb x y. b x y

в теле лямбды перед применением b к x:s происходит (неявное) применение полиморфного значения b : forall a. a -> a -> a к типу s. Эта аппликация терма к типу нужна для того, чтобы <<мономорфизировать>> дотоле полиморфный тип b для дальнейшего использования. Можно эту аппликацию (b s : s -> s -> s) писать явно:

  iif : (forall a. a -> a -> a) -> s -> s -> s
  iif = λb x y. b s x y

UPD. Ну и для полноты картины стоит отметить, что System F должна быть <<оборудована>> ещё и абстракцией терма по типу, которая часто записывается в виде большой лямбды. При этом определение iif принимает окончательный вид

  iif : forall s. (forall a. a -> a -> a) -> s -> s -> s
  iif = Λs. λb x y. b s x y