
Alberto G. Corona wrote:
Wouldn't it be better to achieve the goals you describe with a dependently typed programming language?
But I wonder how a dependent typed language can express certain properties, for example, the distributive property between the operation + and * in a ring or simply the fact that show(read x)==x. As far as I understand, a dependent type system can restrict the set of values for wich a function apply, but it can not express complex relationships between operations.
In a dependently typed language, propositions can be encoded as types, and a value of such a type is a proof that the theorem holds, so one could imagine something like:
class ReadShow a where show :: a -> String read :: String -> Maybe a law :: forall (x : String), read (show x) = x
instance ReadShow Int where show x = <construct string representation of x> read x = <try to parse x> law = <proof of property>
Note that the forall quantifies over values in a type, so this is indeed dependently typed. With the new support for type classes in Coq 8.2, you can write stuff like that.
Require Import List.
Class Monoid (A : Type) := { empty : A; concat : A -> A -> A;
left_ident : forall (a : A), a = concat empty a; right_ident : forall (a : A), a = concat a empty; assoc : forall (a b c : A), concat (concat a b) c = concat a (concat b c) }.
Instance list_monoid : Monoid (list A) := { empty := nil; concat := fun x y => x ++ y;
left_ident := fun a => refl_equal (nil ++ a); right_ident := @app_nil_end A; assoc := @app_ass A }.
The class declaration lists the laws, the instance declaration has to give the proofs. Since these facts about lists are provided by the standard library, this is easy in this example. Of course, one can use the proof mode to prove the laws with a proof script. For example for the Monoid instance for Maybe we have in Haskell.
Instance option_monoid_lifted (A : Type) (MA : Monoid A) : Monoid (option A) := { empty := None; append := fun x y => match (x, y) with | (None, b) => b | (a, None) => a | (Some a, Some b) => Some (append a b) end }. Proof. auto. destruct a; auto. destruct a; destruct b; destruct c; auto. f_equal. apply assoc. Defined.
Tillmann