The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

There is some theory about type-class based monads in math-classes:
http://math-classes.org/

On Thu, Jun 7, 2012 at 5:04 PM, Dmitry Grebeniuk 
<gdsfh1 AT gmail.com>
 wrote:
> Hello.
>
>  I've tried to get support on #coq irc channel, but no one helped,
> so I'm writing here.
>
>  I'm trying to write code in Coq, including the code with error
> handling, with state manipulations, so I chose monads, since
> they work good enough in Haskell world (and I can use well-known
> solutions, even directly translating them to Coq).
>  But I have no hard experience in monads/transformers, also
> I'm newbie in Coq.  So a lot of problems arised, with typeclasses
> especially.  I've tried to solve them by myself, but now I'm completely
> stuck.
>  I've published the code in repository at
> https://bitbucket.org/gds/coq-monads/
> (so you can use "hg clone https://bitbucket.org/gds/coq-monad";
> to clone the repo).
>  The current problem I can't solve is here:
>
> ===============================
> File "./ErrorMonad.v", line 158, characters 4-424:
> Error: In environment
> u : unit
> The term
>  "r <-
>  catch
>    (catch (test1 nil)
>       (fun e : myerr =>
>        match e with
>        | Zero => ret (0 :: nil)
>        | Empty => throw e
>        end))
>    (fun e : myerr =>
>     match e with
>     | Zero => throw e
>     | Empty => b <- lift get;; (if b:bool then 100 :: nil else 200 :: nil)
>     end);; ret (123 :: r)" has type "res myerr (list nat)"
>  while it is expected to have type "stateT bool (stateT bool ?178) ?171".
> make: *** [ErrorMonad.vo] Error 1
> ===============================
>
>  The context is:
>
> ===============================
>  Definition test2 (* : resT _ (State bool) *)
>   :=
>    lift (t := stateT bool) (put true);;
>    r <- catch      (* line 158 *)
>      (catch
>        (test1 nil)
>        (fun e =>
>           match e with
>           | Zero => ret (0 :: nil)
>           | _ => throw e
>           end
>        )
>      )
>      (fun e =>
>         match e with
>         | Empty =>
>             b <- lift $ get;;
>             if b:bool
>             then (100 :: nil)
>             else (200 :: nil)
>         | _ => throw e
>         end
>      );;
>    ret $ 123 :: r
>  .
> ===============================
>
> (this output I got with simple "make" command) -- I can't understand
> why the expression has no type
> "resT myerr (StateMonadT bool Identity)" which should
> be inferred.
>  Adding type constraints make the typechecking fail in other
> pieces of code with other errors.  So I sure that I did wrong
> something.
>  Can you please help me?
>
> //
>  As an addition to the irc message: I've tried to 1. add
> "Typeclasses eauto := debug bfs.", 2. define simpler
> expressions with both ErrorMonadT+(StateT Identity), 3. add
> type annotations to the code.  None of these helped to
> understand the source of problems, which do exist here
> surely.
>
> //
>  As a second addition: I have a question: does anybody write
> a code in Coq with error handling, state and so on?  Are there
> any simple but useful examples?  Maybe I don't need monads
> at all?
>
>  And I'll try to answer before you ask the question about "why
> I need Coq".  I need it for more rich types compared to
> OCaml's types, and to prove some facts about my code.
> Also my employer wants me to use dependent types, so I had
> to chose between Coq and Agda, I chose Coq (since I have
> experience in OCaml and our codebase is in OCaml too,
> and it's easy to integrate Coq here, extraction works just fine).