From: Gabriel Scherer <gabriel.scherer@gmail.com>
To: mukesh tiwari <mukeshtiwari.iiitm@gmail.com>
Cc: caml users <caml-list@inria.fr>
Subject: Re: [Caml-list] Calling Java function from OCaml
Date: Thu, 12 Apr 2018 12:00:29 +0200 [thread overview]
Message-ID: <CAPFanBGgnLm3Z1=WX9h0pjrt=-72_bp-3MNYprz5HKiYTx_2mg@mail.gmail.com> (raw)
In-Reply-To: <CAFHZvE_0v=JjNddjhDfYq4=NyuUoOCKaWRwQscjBQ1KBLrOyJw@mail.gmail.com>
[-- Attachment #1: Type: text/plain, Size: 2837 bytes --]
Remote procedure calls are a generic solution to cross-language
computations that works in many settings. It is a perfectly reasonable
thing to do.
Another option is to use Foreign Function Interfaces on both sides to do
cross-language computation in a single system process (instead of RPCs and
communicating processes). For Java, the FFI layer in the JNI (Java Native
Interface), and there exists a library to make OCaml and Java functions
communicate through the JNI (without changing the OCaml compilation
backend):
https://github.com/xavierleroy/camljava
That said, this library seems to currently lack active users, and in
particular nobody did the work of packaging it on opam (
https://github.com/ocaml/opam-repository/issues/7519 ). If you are willing
to give this library a try, it could be a useful thing to contribute.
In either cases, I would recommend being very careful in designing the
interface between Coq code and untrusted code (pure OCaml, or OCaml+Java
code using whichever coordination system). It is easy to shoot yourself in
the foot by exporting untrusted functions with an optimistic type (eg.
using the Coq function type for the untrusted functions that may not be
total / strongly terminating). If you can design the interface between Coq
and untrusted code as primarily based on exchanging ground *data* (events,
queries reified as algebraic datatypes...), with an explicit loop
orchestrating the coordination between both, you can get a system where the
correctness guarantees (or lack thereof) are much easier to reason about.
Incidentally, this design also makes the in-process data exchange more
similar to what an inter-process communication system would look like, so
it allows implement both solutions (in-process or remote communication)
against a single Coq codebase, with minimal changes.
(As an aside: the #ocaml channel is also populated by experts from the
OCaml community, so its advice is probably as good as the list.)
On Thu, Apr 12, 2018 at 11:40 AM, mukesh tiwari <
mukeshtiwari.iiitm@gmail.com> wrote:
> Hi Everyone,
> I am trying to call some Java functions from OCaml (Extracted from Coq if
> it matters). I am familiar with ocamljava [1], but it says that "*The
> generated code usually runs faster than OCaml bytecode but slower than
> native code. Memory consumption and startup time are also higher, but
> leveraging the multiple cores of a machine can help reaching the
> performance level of native code.*", and I don't want to leave the OCaml
> native code. One suggestion I got on #ocaml channel is using RPC and a
> quick Google search leads to ocaml-rpc [2]. I am wondering if experts from
> OCaml community could please give me some suggestions.
>
>
> Best regards,
> Mukesh Tiwari
>
>
> [1] http://www.ocamljava.org/
> [2] https://github.com/mirage/ocaml-rpc
>
[-- Attachment #2: Type: text/html, Size: 3661 bytes --]
next prev parent reply other threads:[~2018-04-12 10:01 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-04-12 9:40 mukesh tiwari
2018-04-12 10:00 ` Gabriel Scherer [this message]
2018-04-12 19:06 ` forum
2018-04-12 18:57 ` forum
2018-04-13 3:01 ` mukesh tiwari
2018-04-15 18:26 ` forum
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to='CAPFanBGgnLm3Z1=WX9h0pjrt=-72_bp-3MNYprz5HKiYTx_2mg@mail.gmail.com' \
--to=gabriel.scherer@gmail.com \
--cc=caml-list@inria.fr \
--cc=mukeshtiwari.iiitm@gmail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox