In the book Type Theory and Functional Programming [Thompson, S 1999] the author explains the relationship between specifications, types and proofs of functions:

The equivalent specifications can be thought of as suggesting different program development methods: using the ∃∀ form, we develop the function and its proof as separate entities, either separately or together, whilst in the ∀∃ form we extract a function from a proof, post hoc.

This analysis of specifications makes it clear that when we seek a program to meet a specification, we look for the first component of a member of an existential type; the second proves that the program meets the constraint part of the specification.

On this same topic, the commenter writes:

Specifications are in a way "more detailed" types. Or, state the other way, types are more basic specifications. Martin-Lof type theory is precisely about fusing the two ideas into one.

My question is: What is the evidence that that types are more basic specifications, and specifications are more detailed types?

  • 1
    $\begingroup$ What definition of types and specifications are you starting from? (I don't have Thompson's book.) I would define them as synonyms with different connotations, which would make the statement you want evidence for a tautology. $\endgroup$ – Gilles 'SO- stop being evil' Mar 7 '14 at 13:51

As Gilles points out, it depends on what you count as types. If you mean by types something like types in Java or Scala or Haskell, then this is clearly true.

One easy way to see this is (simplifying a bit) to use a general framework of specifications to express the behavioural content of types as a specific case of specification. The best framework to do this at the moment is $\pi$-calculus as a programming language and Hennessy-Milner logic as a specification language. I suggest to choose $\pi$-calculus because it's expressive, and well studied. In particular, most sequential programming languages are easily seen to be (behaviourally equivalent to) specific sub-calculi of $\pi$-calculus. Hennessy-Milner logic is an expressive modal logic that can be used to nail down processes up to behavioural equivalence. Now we take an arbitarty type, say the function space constructor $ int \rightarrow bool $ and express the constraints this type imposes on programs as a specification in Hennessy-Milner logic.

Conversely, we need to show that specifications are strictly more expressive than types but that's fairly obvious, for we cannot specify e.g. that a method is sorting its input array.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.