4 ms·

I'll post a reply that I wrote to one of parent's comments that was deleted, but I think the parent had some reasonable points. It's slightly tweaked to remove

I'll post a reply that I wrote to one of parent's comments that was deleted, but I think the parent had some reasonable points. It's slightly tweaked to remove some of the parts that don't really make sense without the other comment's context. You're implicitly assuming a Curry-style semantics to your language. Here's an outline of what I assume you mean. Correct me if I'm wrong. There are effectively two separate languages. Your type-level language and your term-level language. Each of these languages have their own notions of validity. At the type-level, a series of statements is valid if the type checker accepts them. At the term-level a series of statements is valid if the program runs without crashing. There is also some way of associating the two languages together, i.e. type assignment. Given these two languages, we would like for their two notions of validity to coincide. That is it would be great if given a type assignment, the type-level language is valid (type checker accepts it) if and only if the term-level language is valid (program does not crash). The first thing to note is that many (most?) statically typed languages don't have Curry-style semantics. As UncleMeat points out not crashing is not sufficient to be semantically valid in C++. It might just happen not to crash on your machine with a certain set of optimizations and compiler flags. Types play an integral role in what it means for a language to be semantically valid and it doesn't really make sense to consider the language independently of types. For Curry-style languages, there is an indirect linkage to Godel, but the more obvious link is through the halting problem. If type checking is decidable (something you probably want to be true) then your term-level language must be decidable as well if the two languages truly coincide. But then you lose Turing completeness as your first comment points out. The thing is though that no mainstream statically typed language tries to ensure this. All of them allow assigning a type to something that might loop forever or crash. I would argue you're effectively attacking a straw man of a type system. However, I agree with you that "there are times when a type system is too cumbersome, and we must escape it to do useful things." However, this is not something I view as limited to type systems. I view this as true of every facet of programming (and in a greater sense true of every facet of life). Every system must have a way of piercing its assumptions when you as its user have extra knowledge the system does not. This shows up in performance and protection against side-channel attacks (assembly intrinsics, FFI, etc.). This shows up in orchestration tools (yes yes yes it's all good and well to treat infrastructure as immutable and machines like cattle not pets but I would sometimes like to just SSH onto a machine and make some one-off changes!). This shows up in structured programming (once in a very blue moon Python, it would be great if you just gave me a goto/label). The list goes on and on.

thekhatribharat 7y ago
> There are effectively two separate languages. Your type-level language and your term-level language. Computational Type Theory (CTT) blends the distinction b/w terms and types, and in fact C-H correspondence bears no consequence on CTT research. From a previous comment [1]: > I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance (Church-style) and types that do not (Curry-style), you lack an effective cast escape hatch. I think we've basically two categories of (turing-complete) programming languages: 1. Mainstream languages that use type systems for multiple purposes: operational semantics, compiler optimization, lightweight formal verification, etc, and provide casting escape hatches. 2. Languages where the type system's primary (and only?) purpose is formal verification, and there are no escape hatches. It's just that 1 and 2 are really meant for different domains. 2 is mostly used for high-assurance domains like aerospace, automotive, healthcare, blockchain smart contracts where formal verification is high priority and escape hatches aren't sought, hence not built-in. [1] https://news.ycombinator.com/item?id=22794925 https://news.ycombinator.com/item?id=22794925
somewhereoutth 7y ago
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.

thekhatribharat 7y ago

> There are effectively two separate languages. Your type-level language and your term-level language. Computational Type Theory (CTT) blends the distinction b/w terms and types, and in fact C-H correspondence bears no consequence on CTT research. From a previous comment [1]: > I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance (Church-style) and types that do not (Curry-style), you lack an effective cast escape hatch. I think we've basically two categories of (turing-complete) programming languages: 1. Mainstream languages that use type systems for multiple purposes: operational semantics, compiler optimization, lightweight formal verification, etc, and provide casting escape hatches. 2. Languages where the type system's primary (and only?) purpose is formal verification, and there are no escape hatches. It's just that 1 and 2 are really meant for different domains. 2 is mostly used for high-assurance domains like aerospace, automotive, healthcare, blockchain smart contracts where formal verification is high priority and escape hatches aren't sought, hence not built-in. [1] https://news.ycombinator.com/item?id=22794925 https://news.ycombinator.com/item?id=22794925

somewhereoutth 7y ago

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.