|
|
Re: Can Contracts be Equated with Types?
|
Posted: Aug 10, 2006 11:28 AM
|
|
I'd like to make two points:
First, it's possible to reason about the input/output correctness of algorithms, at least in systems that were designed for this purpose. To illustrate this point, I will prove the >0 output guarantee of the factorial function in one such system, namely Coq (the same one I mentioned before).
First, we define factorial in a straightforward way:
Fixpoint fact (n: nat): nat :=
match n with
| 0 => 1
| S m => (fact m) * n
end.
(nat is the type of natural numbers.)
Next, we formally prove the >0 guarantee in an accompanying lemma:
Lemma fact_result: forall n, (fact n) > 0.
unfold gt.
induction n.
simpl.
apply lt_n_Sn.
simpl.
replace 0 with (0 * fact n).
replace (fact n * S n) with (S n * fact n).
apply mult_lt_compat_r.
apply lt_O_Sn.
assumption.
rewrite mult_comm.
reflexivity.
reflexivity.
Qed.
The proof is pretty unreadable in this form unless one has experience proving things in Coq, but the essence is just proof by induction on n.
The second point I'd like to make is that if the type system is expressive enough, these input/output guarantees can be expressed as types (rather than as accompanying lemma's), exactly like the opening poster theorized.
In Coq, functions whose input/output types incorporate pre- and postconditions are called strongly specified, as opposed to weakly specified functions whose input/output types do not. The fact definition above is an example of a weakly specified function. To illustrate the difference, here's a strongly specified version of fact:
Lemma one_gt_zero: 1 > 0.
unfold gt.
apply lt_n_Sn.
Qed.
Lemma rec_call_valid (rec_val n: nat) (rec_spec: rec_val > 0): (rec_val * S n) > 0.
unfold gt.
intros.
rewrite mult_comm.
replace 0 with (0 * rec_val).
apply mult_lt_compat_r.
apply lt_O_Sn.
assumption.
reflexivity.
Qed.
Fixpoint fact_strong (n: nat): { r: nat | r > 0 } :=
match n with
| 0 => exist _ 1 one_gt_zero
| S m => let (rec_val, rec_spec) := (fact_strong m) in
exist _ (rec_val * (S n)) (rec_call_valid _ _ rec_spec)
end.
The details of what's going on here are unfortunately more complex and involve some Coq specifics, so I won't go into them. The key point however is that the return type has changed from plain nat to { r: nat | r > 0 }, which is a pair-like (and dependent) type consisting of a nat and a proof that said nat is greater than 0. The definition of fact_strong uses the two smaller lemmas (which are now merely implementation details) to produce the result value and the >0 proof simultaneously.
These examples really only show the tip of the iceberg of what's possible. The research field that studies the various interesting relations between type systems, logic, proofs, algorithms, and correctness, is called Type Theory. Before I was introduced to Type Theory, I pretty much had the same gut-feeling as the opening poster about the potential of type systems, and learning about Type Theory was an incredible eye-opener for me.
Unfortunately, all of the above is currently somewhat acedemic; the type systems and formality of semantics of conventional/mainstream programming languages are not nearly expressive or "pure" enough to be able to effectively express let alone prove nontrivial properties of programs written in them.
That said, most programmers probably can't be bothered with all this proving business anyway, although that may be somewhat of a defeatist attitude ;-).
|
|
Previous Topic
