36 ms·

Thankyou for your reply (and apologies for deleting the comment). I am not sure that the distinction between Curry and Church semantics is so critical - after

Thankyou for your reply (and apologies for deleting the comment). I am not sure that the distinction between Curry and Church semantics is so critical - after all we have but a single 'engine of computation': beta reduction, applied to statements in the untyped lambda calculus. Thus a statement with Church annotations will reduce exactly as one without? I think I'm taking the view that statements in the untyped lambda calculus, with beta reduction, are our objects of study, and a type system (Church or Curry derived) is a set of theorems (or indeed a mechanism for generating theorems) that we use to prove certain facts about such objects, again much like the Peano axiomatization of natural numbers. Thus I profess my heresy!

dwohnitmok 7y ago
This is not heresy; it's just Curry. 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. The distinction between Curry and Church semantics does not seem particularly relevant for something like the simply typed lambda calculus. After all f : Int -> Int f(x) = x + 1 f(5) : Int // 6 can simply have its types removed after type checking and everything will still run right? f(x) = x + 1 f(5) // 6 However this distinction becomes more important for type systems with polymorphism, particularly ad-hoc polymorphism. f : a -> b where b is Zeroable f(x) = zero // E.g. List[a] is Zeroable where zero: List[a] = emptyList // Int is Zeroable where zero: Int = 0 // String is Zeroable where zero: String = "" Now an expression such as f(5) is impossible to evaluate without type information. f(5): List[Boolean] // This is emptyList f(5): Int // This is 0 f(5): String // This is "" Types become an essential part of what it means to evaluate a term and hence we are led to Church semantics. Now there are ways of trying to recover Curry-style semantics. One way is to replicate the type system at runtime. Then of course you're free to "erase" the types since you still have them at runtime anyways! This is essentially what statically typed object-oriented languages do with late binding. Note that in the extreme though, the type system cannot limit the scope of valid programs because valid programs at runtime are precisely those valid at type-checking time because the types are replicated! Often though only fragments of the type system will be preserved at runtime so that there is still a discrepancy. For example, usually return type polymorphism (the previous example of f) is disallowed in these systems (see e.g. Java) to avoid having to embed even more of the type system than just the types of individual objects. Another option is to compile the program down into a language with a simpler type system (or no type system at all!) and then use Curry-style semantics with the simpler type system. However, that feels more like an implementation detail than anything else. Just because I can compile Java to C does not mean that they have the same semantics. Indeed the point of compilation is precisely to translate between two systems with incompatible semantics, otherwise the compilation is trivial. Stepping back from all this, Curry-style vs Church-style semantics have implications for type checking and type inference. In general things are harder in a Curry-style regimen. Type-checking which is decidable in a Church system often becomes undecidable in an equivalent Curry system. This makes Curry-style semantics burdensome to work with in rich type systems. Curry-style semantics are of course an ideal fit for gradual typing systems that aim to go from an untyped system and gradually add typing on top of that untyped system.
- somewhereoutth 7y ago
  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.

dwohnitmok 7y ago

This is not heresy; it's just Curry. 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. The distinction between Curry and Church semantics does not seem particularly relevant for something like the simply typed lambda calculus. After all f : Int -> Int f(x) = x + 1 f(5) : Int // 6 can simply have its types removed after type checking and everything will still run right? f(x) = x + 1 f(5) // 6 However this distinction becomes more important for type systems with polymorphism, particularly ad-hoc polymorphism. f : a -> b where b is Zeroable f(x) = zero // E.g. List[a] is Zeroable where zero: List[a] = emptyList // Int is Zeroable where zero: Int = 0 // String is Zeroable where zero: String = "" Now an expression such as f(5) is impossible to evaluate without type information. f(5): List[Boolean] // This is emptyList f(5): Int // This is 0 f(5): String // This is "" Types become an essential part of what it means to evaluate a term and hence we are led to Church semantics. Now there are ways of trying to recover Curry-style semantics. One way is to replicate the type system at runtime. Then of course you're free to "erase" the types since you still have them at runtime anyways! This is essentially what statically typed object-oriented languages do with late binding. Note that in the extreme though, the type system cannot limit the scope of valid programs because valid programs at runtime are precisely those valid at type-checking time because the types are replicated! Often though only fragments of the type system will be preserved at runtime so that there is still a discrepancy. For example, usually return type polymorphism (the previous example of f) is disallowed in these systems (see e.g. Java) to avoid having to embed even more of the type system than just the types of individual objects. Another option is to compile the program down into a language with a simpler type system (or no type system at all!) and then use Curry-style semantics with the simpler type system. However, that feels more like an implementation detail than anything else. Just because I can compile Java to C does not mean that they have the same semantics. Indeed the point of compilation is precisely to translate between two systems with incompatible semantics, otherwise the compilation is trivial. Stepping back from all this, Curry-style vs Church-style semantics have implications for type checking and type inference. In general things are harder in a Curry-style regimen. Type-checking which is decidable in a Church system often becomes undecidable in an equivalent Curry system. This makes Curry-style semantics burdensome to work with in rich type systems. Curry-style semantics are of course an ideal fit for gradual typing systems that aim to go from an untyped system and gradually add typing on top of that untyped system.

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