26 ms·

Types are propositions. See Curry-Howard.

pron 10y ago
Types encode propositions (see Curry-Howard) but are logical judgments in the language's logic. The expression `a:A` does not have a boolean truth value (like a logical proposition), but is rather a judgment. In my example above, the value of the expression `a ∈ B` is true iff a = 3 and false otherwise, but the expression `a:B` is just not a well-formed expression. In other words, you could create a type that corresponds to a proposition, but type assignment is distinct from a proposition (e.g. the proposition `b1 < b2`, assuming `b1,b2:B`) in the language. More precisely, you could say that types encode propositions at the type level (even if the language allows the same data-level syntax in type definitions, as in Idris), while propositions at the data level are distinct, while specs are data level propositions.
- catnaroek 10y ago
  `x:T` is a typing judgment. A typing judgment is not a type, even if one of its constituent parts (`T`) is a type. What you call “data-level propositions” is really just “data-level abstract syntax representation of propositions”. Propositions really are types. (Though, of course, there are types that are not propositions.) And your example is simply not valid Haskell.
  - pron 10y ago
    > A typing judgment is not a type You are absolutely right. `x` is a proof object of `T` in the logic induced by the language, but I didn't want to get to that level of technicality, just to show the difference between data-level propositions and type-level ones. That's why I added the second paragraph, but in the process confused matters; sorry. > Propositions really are types. Types have a syntactic meaning that determines the well-formedness of an expression. Once you talk about types, you must talk about a language; a type cannot exist without a language because it is a syntactic construct, but a proposition can: it is a set (of programs, or Turing machines if you like; people in the verification community may say it's a set of states in a Kripke structure). Now, you could say that given the proposition (or the set) P, you can construct type P in language L that expresses it, but P would still not be a data-level expression in L. You can then argue about whether or not this matters, but you can't deny that the two expressions of proposition, i.e., the dynamic `x < 10` and `T`, are distinct and "live" in two separate worlds. When data-level propositions are concerned, this is not the case. E.g., in TLA+, an untyped logic (TLA+ZFC), the program and the propositions are the very same objects and not at all just a "data-level abstract syntax representation of propositions". > And your example is simply not valid Haskell. It wasn't meant to be (I haven't written a Haskell program in over 15 years). Sadly, unlike standard logic and set notation, there isn't a standard notation for typed LC with data types, or any typed logic for that matter (not one that I'm familiar with), so you have to use something with a meaning people would understand or define a syntax every time.
    - catnaroek 10y ago
      > but a proposition can: it is a set Set theories are normally built on top of the apparatus of logic, so a proposition can't be a set. > (of programs, or Turing machines if you like; people in the verification community may say it's a set of states in a Kripke structure) Ah, I see. You aren't talking about general propositions. You're talking about assertions about program states that can be checked dynamically, but want to verify statically. You can't represent an arbitrary proposition as a data structure, but it's of course a-whole-nother matter if you can decide the proposition's truth value by evaluating a Java expression of type `boolean`. The `boolean` expression itself is still not a proposition, though. > but you can't deny that the two expressions of proposition, i.e., the dynamic `x < 10` and `T`, are distinct and "live" in two separate worlds. Most programming languages don't have propositions at all, for a very good reason: a proposition is the type of a programmer-supplied proof that has no runtime computational relevance, and how to integrate proofs into programming is still a research question whose answer language designers can't wait for. In Java, “the dynamic `x < 10`” is just a `boolean` expression - not a proposition! > E.g., in TLA+, an untyped logic (TLA+ZFC), the program and the propositions are the very same objects and not at all just a "data-level abstract syntax representation of propositions". In TLA+, or any other external program logic, the program itself is just a syntactic object. And by extension so is any `boolean` expression the program might contain. OTOH, if Java had propositions, you could carry out your reasoning internally, side-stepping the need to encode propositions as abstract syntax for a metalanguage to see.
      - pron 10y ago
        > Set theories are normally built on top of the apparatus of logic, so a proposition can't be a set. You don't need a set theory. P is a "naive" set. It's well defined no matter what, because TMs are a recursive set, and P is just a RE subset. You're not in danger of running into any sharp edges. > The `boolean` expression itself is still not a proposition, though. I'm not sure what you mean by that, but I think we're talking past each other. That boolean expression is not a proposition about the program -- that is correct -- but the distinction may be artificial. You may be used to languages where there's a clear distinction between program properties and program code, but if you think about it, that distinction is artificial. For example, the expression `IF x > 0 THEN x ELSE -x` can be understood to be a program description taking the absolute value, but it can also be a proposition, or a description of the set of programs returning the absolute value of their input. Your language may use the same expression in both cases, yet still make a distinction about its meaning based on where it is used. Another language (like TLA+) has no such distinction. > a proposition is the type of a programmer-supplied proof that has no runtime computational relevance That's your definition. For me, a proposition about code is a set of TMs with a property (in particular, safety properties are a closed set of TMs, and liveness properties are dense etc. etc.). Its truth value is whether your program is in this set or not. To be more precise, a proposition to me is a sentence in any logic denoting that set. I think my definition is both more encompassing and more precise than yours. It is more encompassing because every proposition by your definition is a proposition by my definition; it is more precise because the converse may not be true (although, again, I'm not certain about what your definition really means, its ties to a specific language, or whether or not it applies only to denotational semantics of programs). > has no runtime computational relevance I'm not sure what you mean by that. Does the proposition "the program returns a list containing exactly the same elements in its input, each appearing the same number of times, only in sorted order" has a runtime computational relevance or not? > In TLA+, or any other external program logic, the program itself is just a syntactic object. TLA+ is not an external program logic, but a complete logic -- i.e. a TLA+ expression can describe any unique and arbitrary TM, or a set of them -- and there is no difference between a program and a proposition about a program in TLA+. The program is certainly not a syntactic element in TLA+ (certainly no more than any proposition is a syntactic element). Conceptually, in TLA+ you can describe the set of all programs that perform quicksort (it can be more than one; TLA+ allows nondeterminism) and then ask whether quicksort implies sorting, or, in other words, whether the set of quicksort programs is a subset of all programs that sort their input. Both the program and the proposition are logical expressions (describing a set of TMs, if you will), and you may then try to prove that one implies the other (or any logical combination of the two): In a quest for minimality and orthogonality of concepts, TLA+ does not formally distinguish between specifications and properties: both are written as logical formulas, and concepts such as refinement, composition of systems or hiding of internal state are expressed using logical connectives of implication, conjunction, and quantification. Despite its expressiveness, TLA+ is supported by tools such as model checkers and theorem provers to aid a designer carry out formal developments.[1] [1]: http://www.loria.fr/~merz/papers/tla+logic2008.pdf http://www.loria.fr/~merz/papers/tla+logic2008.pdf
catnaroek 10y ago
It's more accurate to say that some types are propositions. More precisely, a type is a proposition if and only if any two inhabitants of it are equal.

pron 10y ago

Types encode propositions (see Curry-Howard) but are logical judgments in the language's logic. The expression `a:A` does not have a boolean truth value (like a logical proposition), but is rather a judgment. In my example above, the value of the expression `a ∈ B` is true iff a = 3 and false otherwise, but the expression `a:B` is just not a well-formed expression. In other words, you could create a type that corresponds to a proposition, but type assignment is distinct from a proposition (e.g. the proposition `b1 < b2`, assuming `b1,b2:B`) in the language. More precisely, you could say that types encode propositions at the type level (even if the language allows the same data-level syntax in type definitions, as in Idris), while propositions at the data level are distinct, while specs are data level propositions.

catnaroek 10y ago
`x:T` is a typing judgment. A typing judgment is not a type, even if one of its constituent parts (`T`) is a type. What you call “data-level propositions” is really just “data-level abstract syntax representation of propositions”. Propositions really are types. (Though, of course, there are types that are not propositions.) And your example is simply not valid Haskell.
- pron 10y ago
  > A typing judgment is not a type You are absolutely right. `x` is a proof object of `T` in the logic induced by the language, but I didn't want to get to that level of technicality, just to show the difference between data-level propositions and type-level ones. That's why I added the second paragraph, but in the process confused matters; sorry. > Propositions really are types. Types have a syntactic meaning that determines the well-formedness of an expression. Once you talk about types, you must talk about a language; a type cannot exist without a language because it is a syntactic construct, but a proposition can: it is a set (of programs, or Turing machines if you like; people in the verification community may say it's a set of states in a Kripke structure). Now, you could say that given the proposition (or the set) P, you can construct type P in language L that expresses it, but P would still not be a data-level expression in L. You can then argue about whether or not this matters, but you can't deny that the two expressions of proposition, i.e., the dynamic `x < 10` and `T`, are distinct and "live" in two separate worlds. When data-level propositions are concerned, this is not the case. E.g., in TLA+, an untyped logic (TLA+ZFC), the program and the propositions are the very same objects and not at all just a "data-level abstract syntax representation of propositions". > And your example is simply not valid Haskell. It wasn't meant to be (I haven't written a Haskell program in over 15 years). Sadly, unlike standard logic and set notation, there isn't a standard notation for typed LC with data types, or any typed logic for that matter (not one that I'm familiar with), so you have to use something with a meaning people would understand or define a syntax every time.
  - catnaroek 10y ago
    > but a proposition can: it is a set Set theories are normally built on top of the apparatus of logic, so a proposition can't be a set. > (of programs, or Turing machines if you like; people in the verification community may say it's a set of states in a Kripke structure) Ah, I see. You aren't talking about general propositions. You're talking about assertions about program states that can be checked dynamically, but want to verify statically. You can't represent an arbitrary proposition as a data structure, but it's of course a-whole-nother matter if you can decide the proposition's truth value by evaluating a Java expression of type `boolean`. The `boolean` expression itself is still not a proposition, though. > but you can't deny that the two expressions of proposition, i.e., the dynamic `x < 10` and `T`, are distinct and "live" in two separate worlds. Most programming languages don't have propositions at all, for a very good reason: a proposition is the type of a programmer-supplied proof that has no runtime computational relevance, and how to integrate proofs into programming is still a research question whose answer language designers can't wait for. In Java, “the dynamic `x < 10`” is just a `boolean` expression - not a proposition! > E.g., in TLA+, an untyped logic (TLA+ZFC), the program and the propositions are the very same objects and not at all just a "data-level abstract syntax representation of propositions". In TLA+, or any other external program logic, the program itself is just a syntactic object. And by extension so is any `boolean` expression the program might contain. OTOH, if Java had propositions, you could carry out your reasoning internally, side-stepping the need to encode propositions as abstract syntax for a metalanguage to see.
    - pron 10y ago
      > Set theories are normally built on top of the apparatus of logic, so a proposition can't be a set. You don't need a set theory. P is a "naive" set. It's well defined no matter what, because TMs are a recursive set, and P is just a RE subset. You're not in danger of running into any sharp edges. > The `boolean` expression itself is still not a proposition, though. I'm not sure what you mean by that, but I think we're talking past each other. That boolean expression is not a proposition about the program -- that is correct -- but the distinction may be artificial. You may be used to languages where there's a clear distinction between program properties and program code, but if you think about it, that distinction is artificial. For example, the expression `IF x > 0 THEN x ELSE -x` can be understood to be a program description taking the absolute value, but it can also be a proposition, or a description of the set of programs returning the absolute value of their input. Your language may use the same expression in both cases, yet still make a distinction about its meaning based on where it is used. Another language (like TLA+) has no such distinction. > a proposition is the type of a programmer-supplied proof that has no runtime computational relevance That's your definition. For me, a proposition about code is a set of TMs with a property (in particular, safety properties are a closed set of TMs, and liveness properties are dense etc. etc.). Its truth value is whether your program is in this set or not. To be more precise, a proposition to me is a sentence in any logic denoting that set. I think my definition is both more encompassing and more precise than yours. It is more encompassing because every proposition by your definition is a proposition by my definition; it is more precise because the converse may not be true (although, again, I'm not certain about what your definition really means, its ties to a specific language, or whether or not it applies only to denotational semantics of programs). > has no runtime computational relevance I'm not sure what you mean by that. Does the proposition "the program returns a list containing exactly the same elements in its input, each appearing the same number of times, only in sorted order" has a runtime computational relevance or not? > In TLA+, or any other external program logic, the program itself is just a syntactic object. TLA+ is not an external program logic, but a complete logic -- i.e. a TLA+ expression can describe any unique and arbitrary TM, or a set of them -- and there is no difference between a program and a proposition about a program in TLA+. The program is certainly not a syntactic element in TLA+ (certainly no more than any proposition is a syntactic element). Conceptually, in TLA+ you can describe the set of all programs that perform quicksort (it can be more than one; TLA+ allows nondeterminism) and then ask whether quicksort implies sorting, or, in other words, whether the set of quicksort programs is a subset of all programs that sort their input. Both the program and the proposition are logical expressions (describing a set of TMs, if you will), and you may then try to prove that one implies the other (or any logical combination of the two): In a quest for minimality and orthogonality of concepts, TLA+ does not formally distinguish between specifications and properties: both are written as logical formulas, and concepts such as refinement, composition of systems or hiding of internal state are expressed using logical connectives of implication, conjunction, and quantification. Despite its expressiveness, TLA+ is supported by tools such as model checkers and theorem provers to aid a designer carry out formal developments.[1] [1]: http://www.loria.fr/~merz/papers/tla+logic2008.pdf http://www.loria.fr/~merz/papers/tla+logic2008.pdf

catnaroek 10y ago

It's more accurate to say that some types are propositions. More precisely, a type is a proposition if and only if any two inhabitants of it are equal.