This seems like a rather lacking write-up, particularly the comparison section and onwards. Why is “supporting new shapes” only discussed for two of the approaches, what about the other two? What is the bit on collections even supposed to mean? How does adding a diffing operation fail for any of the approaches? Surely it’s possible to define a diffing operation somehow, it’s just the conciseness or clarity that’s of question? And finally the new approach is claimed to “fare better” without showing how.

A common real-world example for Church encoding in Haskell is parsing monads. Both parsec and megaparsec use it. My understanding is that GHC does a great job of inlining functions, so higher order parser combinators end up being better optimized. For instance:

newtype ParsecT s u m a
    = ParsecT {unParser :: forall b .
                 State s u
              -> (a -> State s u -> ParseError -> m b) -- consumed ok
              -> (ParseError -> m b)                   -- consumed err
              -> (a -> State s u -> ParseError -> m b) -- empty ok
              -> (ParseError -> m b)                   -- empty err
              -> m b
             }