1
$\begingroup$

Good programming practice distinguishes between specification (at the API level) and implementation. I would have thought that this same distinction would be found in type theory. Perhaps I just don't understand what I'm reading, but I don't see it.

Apologies if I'm completely off (and corrections appreciated), but it seems that in type theory one adds new computation/rewrite rules, which in effect are at the implementation level, i.e., they compute something. (They may be "declarative," but they are used for computation.) I don't see how one adds anything like a specification.

$\endgroup$
  • 1
    $\begingroup$ I'm not an expert, but afaik types provide neither specification nor implementation. $\endgroup$ – Raphael Aug 9 '14 at 21:37
  • $\begingroup$ Pretty sure you're looking for existential types. "Modern" module systems such as those find in some ML family languages make use of them. $\endgroup$ – Steven Shaw Aug 10 '14 at 4:01
  • $\begingroup$ Both off the mark, actually. $\endgroup$ – Andrej Bauer Aug 10 '14 at 9:01
  • $\begingroup$ @RussAbbott: I usually associate "rewrite rules" with programming language semantics. If you are talking about programming language semantics, I agree with you. Operational semantics and denotational semantics are basically implementations (albeit non-deterministic implementations.) If you are actually talking about type theory then I have no clue. Perhaps an example? $\endgroup$ – Wandering Logic Aug 10 '14 at 12:59
3
$\begingroup$

A type $T$ is a specification. A term $t$ of type $T$ is an implementation together with a proof of correctness.

Dependent types are more expressive than simple types found in programming languages. Via the propositions-as-types correspondence they allow us to express logical statements which comprise a specification, rather than just "bare" typing information.

For instance, the type $$\prod_{k : \mathbb{N}} \sum_{m : \mathbb{N}} \mathsf{prime}(m) \times (k < m)$$ can be read in any of the following ways:

  1. As a proposition: for every natural number $k$ there is a prime $m$ larger than $k$.
  2. As a type: the type of functions which take as input a number $k$ and output a triple $(m, p, q)$ where $m$ is a number, $p$ is a proof that $m$ is prime, and $q$ is a proof that $k < m$.
  3. As a specification: implement a function which takes a number and returns a prime larger than it.

Fancier specifications can be expressed just as well. For instance, we can express the specification for a dictionary as a dependent sum (or a record type if it's available) $$\sum_{D : \mathsf{Type}} \sum_{K : \mathsf{Type}} \sum_{V : \mathsf{Type}} \sum_{\mathsf{empty} : D} \sum_{\mathsf{add} : K \to V \to D \to D} \sum_{\mathsf{lookup} : K \to D \to 1 + V} \cdots $$ which is read as follows: we need to specify the type of dictionaries $D$, the type of keys $K$, the type of values $V$, the empty dictionary, and the addition and lookup functions. The $\cdots$ would express the required properties of dictionaries, i.e., logical statements governing the behavior of a dictionary.

$\endgroup$
  • $\begingroup$ Thanks @Andrej_Bauer. It would be difficult to do this in a comment, but would you mind elaborating on how one does the three readings. I see how the first one works. It looks like the third reading is essentially a variant of the second. The specification and the type are both descriptions of the desired function(s). (But why does the third reading not include p and q as output?) $\endgroup$ – RussAbbott Aug 10 '14 at 17:58
  • $\begingroup$ When expressed in a programming language, the input k would be declared of type N. The function would be declared to return an N. (Effectively that takes care of the Pi and Sigma, right?) I'm not sure how you would output p and q. The simplest version of the function would enumerate N until m is found (if ever) that satisfies the two conditions. Isn't that implicit in the Sigma? $\endgroup$ – RussAbbott Aug 10 '14 at 18:10
  • $\begingroup$ You would not output $p$ and $q$ in a programming language, because in general such $p$ and $q$ may not make a lot of sense as data in a programming language. In Coq $p$ and $q$ are elements of $\mathsf{Prop}$, which is erased during program extraction: that is, $p$ and $q$ should exist, but they are not part of the program or the computation proper. They are "on the side". $\endgroup$ – Andrej Bauer Aug 10 '14 at 22:03
  • $\begingroup$ To answer your other question: when we say "returns a prime larger than it" that's just a shorthand for "returns a number such that the number is primer and the number is larger than it". So you can see that we hid $p$ and $q$ in the manner of speech. $\endgroup$ – Andrej Bauer Aug 10 '14 at 22:04

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.