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 <>
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.