Пример теоремы Черча-Россера на языке функционального программирования

Я видел многочисленные ссылки на теорему Черча Россераи, в частности, на диаграмму свойств алмаза, изучая функциональное программирование, но я не наткнулся на хороший пример кода.

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

Я бы дал бонусные баллы, если бы пример легко показывал, как шаги или сокращения приводят к легкому распараллеливанию выполнения.