3 ms·

This is not correct. Thank you for seeking to educate me about dependent typing, but I have a Masters in PL theory, have done numerous proofs about PL and type

This is not correct. Thank you for seeking to educate me about dependent typing, but I have a Masters in PL theory, have done numerous proofs about PL and type theory in Coq, and did my Masters' thesis on contract systems, under the person who invented contracts in higher-order languages. I do, in fact, know what I'm talking about. :) Unfortunately, it is quite a long explanation and needs a full blog post to cover in detail. A few notes, though: contracts can feature blame, which types cannot, and types are proofs and contracts aren't (which can be both a plus and a minus depending on your situation).

chrismonsanto 13y ago
Another PL theory person checking in... - The word 'contract' has different meanings depending on which subcommunity you are talking to. For example, the Penn crowd often uses the word 'contract' in relation to refinement typing. The Scheme folks tend to think of the problem in different terms, but I am not convinced there is any substantial or insightful difference between the various definitions. As you seem to be an expert in the subject, I am sure you have read the manifest contracts paper, but I will leave this link here for the others: http://www.cis.upenn.edu/~mgree/papers/popl2010_contracts.pdf http://www.cis.upenn.edu/~mgree/papers/popl2010_contracts.pd.... - I have never heard anyone say that types cannot feature blame. I would argue that, for example, Haskell's type checker is quite good at blaming the correct party for a type violation. To argue the opposite you would need a precise definition of blame, and I am aware there are several papers written on this subject. I am sure you could find a definition of blame that excludes static type systems, but I am not sure that definition would be useful. - Types are not proofs, but typing derivations are. Even if you consider types and contracts to be different, the execution trace serves as a proof of a dynamically checked 'contract' (which is really just a derivation in an operational semantics).
- catnaroek 13y ago
  dang, ninja'd me
- Locke1689 13y ago
  Types are not proofs, but typing derivations are. This is definitely true, thanks for the correction. I have never heard anyone say that types cannot feature blame. I would argue that, for example, Haskell's type checker is quite good at blaming the correct party for a type violation. I agree this is dependent on how you construct blame. In the sense I was talking about, it would be difficult to construct a type system which blamed in the same way -- the type system would essentially require a runtime checker for independent pieces of the program crossing the contract boundary, which I have seen constructions of, but is generally not seen as standard. For background, my contract work was in Racket, so I am of the Scheme school :)
catnaroek 13y ago
Types themselves are not proofs. In particular, the proposition associated to a type might be a blatant lie - you simply should be unable to find a term for that type. Also, the notion of blame in a contract maps directly to the type checker telling you which term does not type check.

chrismonsanto 13y ago

Another PL theory person checking in... - The word 'contract' has different meanings depending on which subcommunity you are talking to. For example, the Penn crowd often uses the word 'contract' in relation to refinement typing. The Scheme folks tend to think of the problem in different terms, but I am not convinced there is any substantial or insightful difference between the various definitions. As you seem to be an expert in the subject, I am sure you have read the manifest contracts paper, but I will leave this link here for the others: http://www.cis.upenn.edu/~mgree/papers/popl2010_contracts.pdf http://www.cis.upenn.edu/~mgree/papers/popl2010_contracts.pd.... - I have never heard anyone say that types cannot feature blame. I would argue that, for example, Haskell's type checker is quite good at blaming the correct party for a type violation. To argue the opposite you would need a precise definition of blame, and I am aware there are several papers written on this subject. I am sure you could find a definition of blame that excludes static type systems, but I am not sure that definition would be useful. - Types are not proofs, but typing derivations are. Even if you consider types and contracts to be different, the execution trace serves as a proof of a dynamically checked 'contract' (which is really just a derivation in an operational semantics).

catnaroek 13y ago
dang, ninja'd me
Locke1689 13y ago
Types are not proofs, but typing derivations are. This is definitely true, thanks for the correction. I have never heard anyone say that types cannot feature blame. I would argue that, for example, Haskell's type checker is quite good at blaming the correct party for a type violation. I agree this is dependent on how you construct blame. In the sense I was talking about, it would be difficult to construct a type system which blamed in the same way -- the type system would essentially require a runtime checker for independent pieces of the program crossing the contract boundary, which I have seen constructions of, but is generally not seen as standard. For background, my contract work was in Racket, so I am of the Scheme school :)

catnaroek 13y ago

Types themselves are not proofs. In particular, the proposition associated to a type might be a blatant lie - you simply should be unable to find a term for that type. Also, the notion of blame in a contract maps directly to the type checker telling you which term does not type check.