Язык с нормальным порядком редукции?

Необходим язык с нормальным порядком редукции. Такой, чтобы в нем можно было корректно вычислять выражения типа
(λx.y)((λx.xxx)(λx.xxx))

и проверять работоспособность более полезных конструкций, например, рекурсивных лямбда-термов, определенных с помощью Y-комбинатора. Таковые, как известно, способны на очень многое, от простых рекурсивных расчетов факториала до реализации алгоритмов типа foldr, map, filter etc с последующим использованием их для создания еще более сложных конструкций. Порядок редукции и в Lisp, и в Scheme аппликативный, что делает их непригоднымы. Так называемый lazy-диалект Scheme в DrRacket также успешно зацикливается на приведенном выше примере. Возможно, спасение существует в Haskell, тот таки должен для выражения вроде терма в правой части примера лишь создать thunk и благополучно его не вычислять, редуцируя целое выражение, но Haskell имеет строгую и сложную систему типов — он построен на идеях типизированного лямбда-исчисления. А, как известно, тип уже ω-комбинатора λx.xx невычислим. О чем Haskell и заявляет, указывая, что не способен вычислить бесконечно-рекурсивный тип. Вероятно, это возможно победить с использованием расширений типовой системы, как стандартной, так и Glasgo, (существует поддержка т.н. GADT, ключевых слов forall и exists (ага, это именно кванторы)), но очень не хочется убивать приличный объем времени на изучение этих вещей, как и на столь сложную реализацию столь простых идей. Может быть, кто то владеет этими расширениями в Haskell? Или знает подходящий язык? Он может быть сколь угодно игрушечным, всего лишь нужен нормальный порядок редукции. Заранее спасибо.