3 ms·

I'm sorry but this is wrong: "The assertion that beta reduction (i.e. evaluation) does not rely on type information and types are overlaid on top is precisely t

I'm sorry but this is wrong: "The assertion that beta reduction (i.e. evaluation) does not rely on type information and types are overlaid on top is precisely the heart of Curry semantics." Beta reduction is not affected by types ascribed to terms. The crucial difference between Church and Curry is that Curry allows each term to be ascribed a set of types - perhaps 0, 1 or many - whereas Church insists on each term having exactly one (often annotated). That is all. Both are systems for proving type correctness of terms, and are no more than that.

somewhereoutth 7y ago
(cont'd) ... and I see it now, the damage that has been wrought. I imagine Church never dreamed that his approach of unitary type assignment would lead people to believe that types actually exist, and that programs should do different things when meeting such 'types'. Yes let's get back to Curry, and build a better world.
- dwohnitmok 7y ago
  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.

somewhereoutth 7y ago

(cont'd) ... and I see it now, the damage that has been wrought. I imagine Church never dreamed that his approach of unitary type assignment would lead people to believe that types actually exist, and that programs should do different things when meeting such 'types'. Yes let's get back to Curry, and build a better world.

dwohnitmok 7y ago
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.