The Coq mailing list

[Julien Narboux <jnarboux AT narboux.fr>]

2012/6/7 Dmitry Grebeniuk <gdsfh1 AT gmail.com>

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?

Xavier Leroy is using the Error monad in CompCert. This comes together with nice notations.

Julien

 

 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).