# What is the evidence that that types are more basic specifications, and specifications are more detailed types?

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?

• 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. Mar 7 '14 at 13:51

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.