[Haskell-cafe] Haskell.org GSoC
Tillmann Rendel
rendel at cs.au.dk
Thu Feb 19 15:56:04 EST 2009
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
More information about the Haskell-Cafe
mailing list