Код, реализующий уникальные возможности каждого ребра лямбда-исчисления

Я не могу объяснить термин лямбда-куб намного лучше, чем это делает Википедия:

{{1} }

[...] λ-куб представляет собой основу для исследования осей уточнения в исчислении конструкций Кокванда, начиная с просто типизированного лямбда-исчисления как вершины куб помещен в начало координат, а исчисление конструкций (полиморфное лямбда-исчисление более высокого порядка) в качестве его диаметрально противоположной вершины. Каждая ось куба представляет новую форму абстракции:

• Термины, зависящие от типов или полиморфизма. Система F, также известная как лямбда-исчисление второго порядка, получается путем наложения только этого свойства.
• Типы в зависимости от типов или операторов типа. Просто типизированное лямбда-исчисление с операторами типа λω получается путем наложения только этого свойства. В сочетании с Системой F это дает Систему Fω.
• Типы в зависимости от условий или зависимые типы. Наложение только этого свойства дает λΠ, систему типов, тесно связанную с LF.

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

Можно ли найти примеры кода на таких языках, как Java, Scala, Haskell, Agda, Coq для каждого уточнения, которое было бы невозможно достичь в вычислениях без этого уточнения?