About Purity

About Purity

[Pierre-Evariste Dagand]

Hi list,

I'm looking for advices, especially from Computer Scientists using
OCaml as a language for their research works.

Here is my situation: I have worked on a system that relies on a
purely functional structure, let say a monad.
At the end, I have come up with a paper explaining how good and great
my work is ;-)
And finally, in order to get some feedback, my paper has been reviewed
by a Haskeller.

Here starts the issues :-)

Using OCaml in combination with a quite strange monad scared the
Haskeller. Indeed, as OCaml does not ensure referential transparency,
there is no formal proof that I'm pure and that what I have used is
truly a monad. And, no way, I did not succeed in convincing him that
my code is pure.

Nonetheless, I know that there are a lot of works in functional
programming that are carried out in OCaml.

So, my question is :

How do you convince these fanatics ;-) that you are pure ?


Obviously, I could show my code but it's about 2kloc that must be pure.

I am considering to re-write my system or at least the purely
functional subset in Haskell. But OCaml is like a mother tongue to me
so that's quite hard (sentimentally speaking) to leave it without
invoking the wisdom of its gurus.

Best regards,

-- 
Pierre-Evariste DAGAND

Re: [Caml-list] About Purity

[Pierre-Evariste Dagand]

> I think if your code
> [snip]
>
> This should be a proof that your code is pure ?

Sure, with some hackery this might be doable. And this would provide
an informal proof (weaker than something ensured by a (hopefully)
sound typechecker).

But the :

> - maybe one or two other conditions that I miss ?

will upset any Haskeller :-)

> Maybe someone could/has implement/ed a purity check for OCaml ? Or even
> better a patch to have
> the pure subset of OCaml with an optimized GC (no more list of greyval),
> that would be nice !

Indeed, that's would be very helpful. In fact, I was so desperate to
have to leave OCaml that I have considered a kind of "pure" (O)Caml.
But now that I'm sober, erf...

Nonetheless, that's an interesting food for thoughts.

> I think this would be a complete loss of time ! Moreover 2kloc is not so
> much so the referee could
> look at it ?

I have no experience as a referee as well as a "reviewed" (that's my
first submission in a FP conference) but I use to think that if things
are not clear, the referee will simply drop the paper.

And, as I mentioned, my functional structure is quite unusual so that
I have to be very convincing.

Thanks for your suggestions,
Best regards,

-- 
Pierre-Evariste DAGAND