5 ms·

(Static) types may be seen as propositions, but this is just one interpretation of them. We can also interpret types as sets (although this doesn't work out ver

by rntz 10y ago

(Static) types may be seen as propositions, but this is just one interpretation of them. We can also interpret types as sets (although this doesn't work out very well except in very simple languages), as domains (most commonly), as cpos, as relations over closed terms (PERs), and so forth. The types-as-propositions interpretation is a particularly useful one because it lets us take ideas from the field of formal logic and apply them to programming. But it is only one interpretation, and not a definition of what types are. I don't think it's possible to give "type" a good, short definition. For me John Reynolds' definition comes closest: "Type structure is a syntactic discipline for enforcing levels of abstraction." But that's rather a mouthful, and not a good introduction to what types are. > A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition. The type that an expression or variable has does not correspond to the proposition that that expression has a certain set of possible values! You're mixing the object-level (the language & its types) with the meta-level (assertions about the language). This is a total misunderstanding of Curry-Howard. Rather, the values an expression might take on can be interpreted as proofs of the corresponding proposition.

naasking 10y ago
> (Static) types may be seen as propositions, but this is just one interpretation of them. We can also interpret types as sets (although this doesn't work out very well except in very simple languages), as domains (most commonly), as cpos, as relations over closed terms (PERs), and so forth. Right, I wasn't advancing the propositional definition as the only one, merely as one that sufficiently captures the generality, because the article's current definition of types-as-sets is insufficiently general.
- catnaroek 10y ago
  Under HoTT's take on propositions as “types where any two inhabitants are equal”, “types as propositions” is even less general than “types as sets”. As I stated in a comment on that gist, what types denote varies from one type system to another: https://gist.github.com/garybernhardt/122909856b570c5c457a6cd674795a9c?#gistcomment-1856634 https://gist.github.com/garybernhardt/122909856b570c5c457a6c...
  - naasking 10y ago
    No one except mathematicians and type theorists are using HoTT, where every programmer in existence is using first-order and sometimes second-order logic. I think it should be obvious which is more appropriate if this is supposed to be an introduction. The idea that types express propositions in first- or second-order logic about a program one is writing is sufficiently general for every programmer to understand the proper scope of type checking. Types-as-sets is simply false as an introductory concept.
    - catnaroek 10y ago
      > No one except mathematicians and type theorists are using HoTT, Right. > where every programmer in existence is using first-order and sometimes second-order logic. I'm not so sure about this one. Perhaps by “programmer” you mean “every Haskell programmer”? Even then I'm still not sure. Are you counting “let's approximate `forall x. P(x)` with the large but finite conjunction `P(a) /\ P(b) /\ P(c) ...`” as “using first-order logic”?
      - naasking 10y ago
        I mean pretty much every programmer, even C programmers. Simple business logic is rife with such propositions. Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs Haskell programmers also use higher order logic, which is also common now in Java and C#.
        catnaroek 10y ago
        > Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs I wasn't talking about types either. Most programmers I've talked to simply can't use formal logic.
        naasking 10y ago
catnaroek 10y ago
> For me John Reynolds' definition comes closest: "Type structure is a syntactic discipline for enforcing levels of abstraction." But that's rather a mouthful, and not a good introduction to what types are. The nice thing about this definition is that it reveals why reflection renders a type system useless: it destroys the type system's ability to enforce abstractions.
eli_gottlieb 10y ago
>The types-as-propositions interpretation is a particularly useful one because it lets us take ideas from the field of formal logic and apply them to programming. But it is only one interpretation, and not a definition of what types are. Ehhh, it kind of is a definition. Think of it this way: a type system is a topology we lay over programs, with open sets representing observable (using finite computation) properties and closed sets representing deniable (using finite computation) properties. The finest such topology possible is the Scott topology, which can distinguish every single observable value and deniable property from every other: it encodes all the information you can have about a program without solving the Halting Problem. Type systems, then, are coarser topologies over programs than that one, which group observably different expressions and traces into the same open sets, which are then called "types". When those types are guaranteed not to contain _|_, the divergent program, they can also be considered topological spaces, with the programs in them acting as points in the topological space.

by rntz 10y ago

naasking 10y ago

> (Static) types may be seen as propositions, but this is just one interpretation of them. We can also interpret types as sets (although this doesn't work out very well except in very simple languages), as domains (most commonly), as cpos, as relations over closed terms (PERs), and so forth. Right, I wasn't advancing the propositional definition as the only one, merely as one that sufficiently captures the generality, because the article's current definition of types-as-sets is insufficiently general.

catnaroek 10y ago
Under HoTT's take on propositions as “types where any two inhabitants are equal”, “types as propositions” is even less general than “types as sets”. As I stated in a comment on that gist, what types denote varies from one type system to another: https://gist.github.com/garybernhardt/122909856b570c5c457a6cd674795a9c?#gistcomment-1856634 https://gist.github.com/garybernhardt/122909856b570c5c457a6c...
- naasking 10y ago
  No one except mathematicians and type theorists are using HoTT, where every programmer in existence is using first-order and sometimes second-order logic. I think it should be obvious which is more appropriate if this is supposed to be an introduction. The idea that types express propositions in first- or second-order logic about a program one is writing is sufficiently general for every programmer to understand the proper scope of type checking. Types-as-sets is simply false as an introductory concept.
  - catnaroek 10y ago
    > No one except mathematicians and type theorists are using HoTT, Right. > where every programmer in existence is using first-order and sometimes second-order logic. I'm not so sure about this one. Perhaps by “programmer” you mean “every Haskell programmer”? Even then I'm still not sure. Are you counting “let's approximate `forall x. P(x)` with the large but finite conjunction `P(a) /\ P(b) /\ P(c) ...`” as “using first-order logic”?
    - naasking 10y ago
      I mean pretty much every programmer, even C programmers. Simple business logic is rife with such propositions. Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs Haskell programmers also use higher order logic, which is also common now in Java and C#.
      - catnaroek 10y ago
        > Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs I wasn't talking about types either. Most programmers I've talked to simply can't use formal logic.
        naasking 10y ago

catnaroek 10y ago

> For me John Reynolds' definition comes closest: "Type structure is a syntactic discipline for enforcing levels of abstraction." But that's rather a mouthful, and not a good introduction to what types are. The nice thing about this definition is that it reveals why reflection renders a type system useless: it destroys the type system's ability to enforce abstractions.

eli_gottlieb 10y ago

>The types-as-propositions interpretation is a particularly useful one because it lets us take ideas from the field of formal logic and apply them to programming. But it is only one interpretation, and not a definition of what types are. Ehhh, it kind of is a definition. Think of it this way: a type system is a topology we lay over programs, with open sets representing observable (using finite computation) properties and closed sets representing deniable (using finite computation) properties. The finest such topology possible is the Scott topology, which can distinguish every single observable value and deniable property from every other: it encodes all the information you can have about a program without solving the Halting Problem. Type systems, then, are coarser topologies over programs than that one, which group observably different expressions and traces into the same open sets, which are then called "types". When those types are guaranteed not to contain _|_, the divergent program, they can also be considered topological spaces, with the programs in them acting as points in the topological space.