Stream: Coq users

Topic: OCaml signatures in Coq


view this post on Zulip MMY MMY (Apr 03 2022 at 21:09):

Hi,
Is the notion of signature present in OCaml also implemented in Coq?

view this post on Zulip Paolo Giarrusso (Apr 03 2022 at 22:22):

@MMY MMY yes, see Module Type. (but is that related to this thread?)

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Apr 04 2022 at 09:27):

@MMY MMY you're adding your question to a Zulip thread about another question

view this post on Zulip 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

view this post on Zulip MMY MMY (Apr 04 2022 at 10:05):

@Paolo Giarrusso sorry .

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip MMY MMY (Apr 04 2022 at 20:04):

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.

view this post on Zulip MMY MMY (Apr 05 2022 at 08:57):

Do you have specific documentation (course, example, etc.) allowing me to launch my test?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip MMY MMY (Apr 05 2022 at 19:17):

I want to do the same continuation function in Coq.


Last updated: Jan 29 2023 at 05:03 UTC