Ah indeed you're right about beta-reduction; jumping to equating it with general evaluation is a bridge too far. Eh... I dunno. Church was around for a long ti

Ah indeed you're right about beta-reduction; jumping to equating it with general evaluation is a bridge too far. Eh... I dunno. Church was around for a long time. He saw a lot of the languages we use now. That ship for ad hoc polymorphism sailed a long time ago. Almost every widely used language I can think of has ad hoc polymorphism, whether that be through runtime types (late binding a la Python, PHP, Ruby, Common Lisp, Javascript, Java, Clojure, Scala, C#, C++, Smalltalk) or through compile time translation (early binding a la Rust, Haskell, also Scala, ML, also Java, also C++, Idris, Agda, Coq). The only languages I can think of at the moment that doesn't have ad hoc polymorphism are C and Elm. To put it another way every language that supports some notion of overloading has to do a different thing when meeting a type. And I think you'd have a hard time taking overloading away from programmers.