A language with normal order of reduction?

Question

Functional programming

We need a language with a normal order of reduction. Such that it can correctly evaluate expressions like
(λx.y)((λx.xxx)(λx.xxx))
and check the performance of more useful constructs, such as recursive lambda terms defined using the Y-combinator. Those are known to be capable of a lot, from simple recursive factorial calculations to implementing algorithms like foldr, map, filter etc and then using them to create even more complex structures. The order of reduction in both Lisp and Scheme is applicative, which makes them unusable. The so-called lazy dialect Scheme in DrRacket also successfully loops on the above example. Perhaps salvation exists in Haskell, which still has to create a thunk for an expression like a term on the right side of the example and not safely evaluate it, reducing the whole expression, but Haskell has a strict and complex type system - it is built on the ideas of a typed lambda calculus. And, as you know, the type of the already ω-combinator λx.xx is not computable. Which is what Haskell claims when it says it can't compute an infinite-recursive type. It is probably possible to beat this using extensions to the type system, both standard and Glasgo (there is support for the so-called GADT, the keywords forall and exists (yeah, those are quantifiers)), but I really don’t want to kill a decent amount of time on the study of these things, as well as on such a complex implementation of such simple ideas. Maybe someone owns these Haskell extensions? Or knows the right language? It can be arbitrarily toy, just need a normal order of reduction. Thanks in advance. so is Glasgo, (there is support for the so-called GADT, the keywords forall and exists (yeah, these are quantifiers)), but I really don’t want to kill a decent amount of time studying these things, as well as such a complex implementation of such simple ideas. Maybe someone owns these Haskell extensions? Or knows the right language? It can be arbitrarily toy, just need a normal order of reduction. Thanks in advance. so is Glasgo, (there is support for the so-called GADT, the keywords forall and exists (yeah, these are quantifiers)), but I really don’t want to kill a decent amount of time studying these things, as well as such a complex implementation of such simple ideas. Maybe someone owns these Haskell extensions? Or knows the right language? It can be arbitrarily toy, just need a normal order of reduction. Thanks in advance.

Answer 1

O! There was such thing: LCI Very quite not bad for a start.

Answer 2

Some detail was found out: first of all, in the desired language, the performance of the Y-combinator is interesting, since it allows you to solve recursive equations, which, in turn, allows you to create recursive functions. However, despite the formal equality (convertibility) ∀ X ( λ ⊢ YX = _β X (YX) ), neither YX is β-reducible to X (YX), nor vice versa. There is, however, a better in this sense and similar in its practical capabilities Θ-combinator, invented by Alan Turing, as well as many other fixed-point combinators(you can also find many examples of the implementation of combinators in various languages ​​at the link, which is extremely valuable). Their computability, however, is still sensitive to the order of reduction, but the requirement for a normal order is redundant. In addition to the concept of the normal form of a term, there are the concepts of a head (or head) normal form, a weak head normal form, which are used in some languages ​​even with a fundamentally applicative order of reduction and lead to the fact that a term argument, having barely become a λ-abstraction (in a weak case), ceases to be evaluated and is passed to the body of the function (the leftmost outer redex is reduced, as in the normal order). This makes special tricks possible in such languages,

Answer 3

As far as I remember, The Rock meets all your requirements. Yes, typing is static there, but it is she who allows you to set the type of infinite recursion, and lives quite normally with this. I recommend the progfun course on coursera.