coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Monad (Re: [Coq-Club] Unification)

From: David Nowak <David.Nowak AT lsv.ens-cachan.fr>
To: Thery Laurent <thery AT ns.di.univaq.it>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: Monad (Re: [Coq-Club] Unification)
Date: Thu, 03 Feb 2005 17:14:06 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thery Laurent wrote:
> Yes I could have used monad (I've used a simple option type instead) but
> to my knowledge,the extraction would never give you back a code that
> uses directly the exception mechanism of ocaml.

I agree. But if you consider the monad as an abstract data type, you can implement it in OCaml using exceptions from OCaml, can't you?

David.

--
David Nowak
LSV, CNRS UMR 8643 & ENS de Cachan
61, av. du President Wilson, 94235 Cachan Cedex, France
tel: +33 1 47 40 75 47 fax: +33 1 47 40 75 21
http://www.lsv.ens-cachan.fr/~nowak/

[Coq-Club] Unification, Colin Riba
- Re: [Coq-Club] Unification, Claude Marche
  - Re: [Coq-Club] Unification, Thery Laurent
    - Monad (Re: [Coq-Club] Unification), David Nowak
      - Re: Monad (Re: [Coq-Club] Unification), Jean-Christophe Filliatre
      - Re: Monad (Re: [Coq-Club] Unification), Thery Laurent
        
        Re: Monad (Re: [Coq-Club] Unification), David Nowak
- Re: [Coq-Club] Unification, Conor McBride