2 ms·

Another PL theory person checking in... - The word 'contract' has different meanings depending on which subcommunity you are talking to. For example, the Penn

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

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 :)