Встраивание более высоких типов (монад!) В нетипизированное лямбда-исчисление

В нетипизированном лямбда-исчислении можно кодировать различные типы с помощью функций более высокого порядка.

Examples:
zero  = λfx.      x
one   = λfx.     fx
two   = λfx.   f(fx)
three = λfx. f(f(fx))
etc

true  = λtf. t
false = λtf. f

tuple = λxyb. b x y
null  = λp. p (λxy. false)

Мне было интересно, проводилось ли какое-либо исследование по внедрению других, менее традиционных типов. Было бы замечательно, если бы существовала некоторая теорема, утверждающая, что любой тип может быть вложен. Возможно, есть ограничения, например могут быть встроены только типы вида *.

Если действительно возможно представить менее традиционные типы, было бы замечательно увидеть пример. Мне особенно интересно посмотреть, как выглядят члены класса монадных типов.