[Haskell-cafe] Haskell.org GSoC

[Tillmann Rendel]

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