At least in simply-typed lambda calculus it's not possible, see also https://crypto.stanford.edu/~blynn/lambda/simply.html https://crypto.stanford.edu/~blynn/la

At least in simply-typed lambda calculus it's not possible, see also https://crypto.stanford.edu/~blynn/lambda/simply.html https://crypto.stanford.edu/~blynn/lambda/simply.html : > This implies the Y combinator and omega combinator cannot be expressed in this system. […] In other words, programs always halt. I assume the reason you can still write down the type in Haskell (as in your example further down) is that Haskell types include the bottom?