coq-practical-monads /

Filename Size Date modified Message
55 B
444 B
1.2 KB
        Coq Practical Monads Library.

    What is this?

  Library implementing some monads and monad transformers.
Monads are implemented with modules and functors over modules.
Every monad/transformer law is proved.  Monads (except Identity)
are implemented as monad transformers.
  Warning: functional extensionality is used here.  (but it's
the only axiom in this developement.)

    Why "practical"?

  Most of the code that allows one to use monads in Coq fails into
two categories:
  - proof of concept, unusable in practice: no single interface, no
    documentation, ad-hoc solutions, no "download, install and use"
  - attempts to use typeclasses.  (author hadn't heard of successful
    Coq typeclasses applications here.)


  Look at the beginning of src/{Error,State,...}Monad.v file for API
and usage examples.




  Get fresh versions from:

  File bugs / feature requests to:

  Pull requests are welcome too.


  Dmitry Grebeniuk <>
  Wojciech Meyer <>