The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

I'm trying to write a simple example in which I use a monoid typeclass instance, namely { list [A], (app A), (nil A) } as a parameter to a reduce/foldr function. I'm having a little trouble getting overloading to resolve the type of list element (in the example here, it's string). Any help would be appreciated.

Separately, I'd note that the error message produced for the last line of this short code segment is this: Error: The term "append_nil" has type "Monoid" while it is expected to have type "Monoid". This doesn't seem quite right.

Thanks!

Kevin

(* A [Monoid] typeclass on carrier [A] *)

Class Monoid {A: Type} : Type :=

{ 

  dot : A -> A -> A;

  id: A;

  dot_assoc: forall x y z : A, dot x (dot y z) = dot (dot x y) z;

  id_left: forall x, dot id x = x;

  id_right: forall x, dot x id = x 

}.

(** Instance for [list A] with [app] and [nil] *)

Instance append_nil {A: Type}: Monoid  :=

  { dot := @app A; id := nil }.

Proof.

Require Import List.

intros x y z.

generalize dependent A.

exact List.app_assoc.

generalize dependent A.

exact List.app_nil_l.

generalize dependent A.

exact List.app_nil_r.

Defined.

(** * A "safe" foldr function using a Monoid *)

Fixpoint sfoldr {A: Type} (l: list A) (m: Monoid): A :=

  match l with

    | nil => id

    | cons h t => dot h (sfoldr t m)

  end.

Require Import String.

Open Scope string_scope.

Compute sfoldr (cons "Hello " (cons "World!" nil)) append_nil.