MMY MMY (Apr 03 2022 at 21:09): MMY MMY (Apr 03 2022 at 21:09):Hi,
Is the notion of signature present in OCaml also implemented in Coq?
Paolo Giarrusso (Apr 03 2022 at 22:22):@MMY MMY yes, see Module Type. (but is that related to this thread?)
MMY MMY (Apr 04 2022 at 08:11):Thank you. Sorry, I didn't understand your question. Don't we ask here all the questions relating to the Coq?
Paolo Giarrusso (Apr 04 2022 at 09:27):@MMY MMY you're adding your question to a Zulip thread about another question
Karl Palmskog (Apr 04 2022 at 09:29):I changed the topic.
@Paolo Giarrusso feel free to edit topics on your own when you see something like this
MMY MMY (Apr 04 2022 at 10:05):@Paolo Giarrusso sorry .
MMY MMY (Apr 04 2022 at 10:51):I started to learn Coq and I don't understand OCaml very well.
but a code that interests me is written in OCaml and I want to transform it into Coq . Could you give me your opinion on this transformation.
OCaml :
type 'a cont
val callcc: ('a cont -> 'a) -> 'a
val throw: 'a cont -> 'a -> 'b
Coq :
Set Nested Proofs Allowed.
Variable cont : forall (a : Set), Set.
Definition callcc : forall {a : Set}, (cont a -> a) -> a.
Definition throw : forall {a b : Set}, cont a -> a -> b.
Li-yao (Apr 04 2022 at 13:54):That looks almost right but those are the wrong keywords.
Module Type MySig.
Parameter cont : forall (a : Type), Type.
Parameter callcc : forall (a : Type), (cont a -> a) -> a.
Parameter throw : forall (a b : Type), cont a -> a -> b.
End MySig.
Thank you for your reply.
If I understand correctly if I want to run a test like:
Eval compute in (1 + callcc (fun k => 2 + throw k 3)).
I have to go through another statement:
Modulus M<:MySig.
....
End M.
MMY MMY (Apr 05 2022 at 08:57):Do you have specific documentation (course, example, etc.) allowing me to launch my test?
Li-yao (Apr 05 2022 at 12:53):There is a list of introductory materials to learn Coq here https://coq.inria.fr/documentation
Note that module signatures are not at all as necessary as they are in OCaml. Unless you are specifically interested in modules, you can do without. There is also an issue that throw cannot be implemented because Coq is a total language, but you have to walk before you run.
MMY MMY (Apr 05 2022 at 13:01):I am no more interested in modules than in transforming this code into Coq, which is why at the start I translated instruction by instruction.
For the rooster courses I followed a lot from start to finish to work with this particular code.
If you can offer me a track to make this code work I will be very grateful.
Li-yao (Apr 05 2022 at 13:33):Why do you want to translate this code into Coq?
Translating impure languages in Coq is a very broad topic, and especially for features like continuations, there are no straightforward answers. So you might want to reassess what it is that you are trying to do to better focus your research.
MMY MMY (Apr 05 2022 at 19:17):I want to do the same continuation function in Coq.
Last updated: Sep 23 2023 at 14:01 UTC