3 ms·

Well, there isn't any generally accepted definition of what a type system is. _Types and Programming Languages_ (2002) start out with the sentence "a type syste

Well, there isn't any generally accepted definition of what a type system is. _Types and Programming Languages_ (2002) start out with the sentence "a type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute", a definition which is both not very precise ("tractable"?) and is also not general enough to cover dependent types (where we care about both presence and absence of behaviors). Similarly, there isn't really any definition of a logic. Some authors talk about a proof system + a semantics, which is also not precise, and also not general enough (some constructivists don't want the semantics). So it seems hard to do better than this?

deleted 12y ago
[deleted]
JadeNB 12y ago
> "a type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute" … not general enough to cover dependent types (where we care about both presence and absence of behaviors). As someone who's comfortable with an informal approach to mathematical logic but has never done any programming with dependent types, I wonder if this may be hitting on a fundamental point. Certain presences can be interpreted as absences, i.e., the absence of their absence, in just the same way as certain statements can be interpreted as the negations of their negations. (In classical logic, but not in constructivist logic, all statements can be so interpreted.) Is there any chance that the 'presences' needed in dependent type theory are those that can be expressed as the 'absence of an absence' (something like that it is not so important what characteristics an object does have, as what assumptions about the object can't go wrong)?
- vilhelm_s 12y ago
  The "presence" I had in mind was just "this function will eventually return a value", i.e. what you get from having a type for total functions. (On the programming side, this ties into a discussion about "safety" versus "liveness" properties).

deleted 12y ago

[deleted]

JadeNB 12y ago

> "a type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute" … not general enough to cover dependent types (where we care about both presence and absence of behaviors). As someone who's comfortable with an informal approach to mathematical logic but has never done any programming with dependent types, I wonder if this may be hitting on a fundamental point. Certain presences can be interpreted as absences, i.e., the absence of their absence, in just the same way as certain statements can be interpreted as the negations of their negations. (In classical logic, but not in constructivist logic, all statements can be so interpreted.) Is there any chance that the 'presences' needed in dependent type theory are those that can be expressed as the 'absence of an absence' (something like that it is not so important what characteristics an object does have, as what assumptions about the object can't go wrong)?

vilhelm_s 12y ago
The "presence" I had in mind was just "this function will eventually return a value", i.e. what you get from having a type for total functions. (On the programming side, this ties into a discussion about "safety" versus "liveness" properties).