Stream: Coq devs & plugin devs

Topic: Why do we use -rectypes?

Ali Caglayan (Apr 20 2022 at 14:10):

I see that -rectypes came up in discussion again, and the question that has been asked before comes to mind: "Why do we bother with it?". AFAICT https://github.com/ocaml/dune/issues/1420#issuecomment-447734051 contains some of the reasons we still have it. Would it be a good idea to perhaps drop -rectypes from most of the codebase and allow it locally where it is really needed?

Ali Caglayan (Apr 20 2022 at 14:13):

kernel/constr.ml contains the first rectypes need, but I guess this can easily be worked around with the boxing unboxing trick that @Pierre-Marie Pédrot mentioned in the post linked above.

Ali Caglayan (Apr 20 2022 at 14:14):

nativevalues.ml is a different story however and I don't understand what is going on enough to see the problem removing rectypes there.

Pierre-Marie Pédrot (Apr 20 2022 at 14:44):

constr.ml is an implementation file, and the equirecursive type doesn't leak into the interface so actually this does not require any use of -rectypes in the dependencies. We don't even need to box.

Pierre-Marie Pédrot (Apr 20 2022 at 14:44):

For nativevalues, this is needed because we use a "universal" type for untyped objects.

Pierre-Marie Pédrot (Apr 20 2022 at 14:45):

In particular, we must be able to apply any native value to any argument.

Pierre-Marie Pédrot (Apr 20 2022 at 14:46):

Currently this application is transparent, so we must have a functional type somewhere, and the constraints essentially force us to pick t := t -> t.

Pierre-Marie Pédrot (Apr 20 2022 at 14:46):

We could work around this by adding a dummy Obj.magic cast at application time, but this is more tricky than it seems.

Pierre-Marie Pédrot (Apr 20 2022 at 14:47):

Essentially, we must replace the definition t := t -> t with an iso t ≅ t -> t

Pierre-Marie Pédrot (Apr 20 2022 at 14:47):

I tried to do that once, but the problem is that functions have some hardwired properties in OCaml

Pierre-Marie Pédrot (Apr 20 2022 at 14:47):

in particular, the compilation scheme for fixpoint becomes tricky, and there are also issues with value restriction.

Ali Caglayan (Apr 20 2022 at 14:56):

I found another in vernac declare. That one is also probably not needed right?

Pierre-Marie Pédrot (Apr 20 2022 at 14:56):

Which type is that?

Ali Caglayan (Apr 20 2022 at 14:57):

ln 1032

Ali Caglayan (Apr 20 2022 at 14:57):

State.t

Pierre-Marie Pédrot (Apr 20 2022 at 14:57):

Oh, yes, you could box that one.

Ali Caglayan (Apr 20 2022 at 14:59):

What is your suggestion for constr?

Ali Caglayan (Apr 20 2022 at 15:00):

Just inline "constr" everywhere?

Ali Caglayan (Apr 20 2022 at 15:01):

I tried boxing it but I have to change a lot of things

Guillaume Melquiond (Apr 20 2022 at 15:20):

Pierre-Marie Pédrot said:

For nativevalues, this is needed because we use a "universal" type for untyped objects.

Is it actually needed? Sure, you need it for the code generated by native_compute. But wouldn't the code in nativevalues.ml itself be fine with a non-recursive type and a handful of Obj.magic?

Pierre-Marie Pédrot (Apr 20 2022 at 15:22):

No, that's not needed, that's my point.

Pierre-Marie Pédrot (Apr 20 2022 at 15:22):

I have a branch somewhere that tried that, I can unearth it.

Guillaume Melquiond (Apr 20 2022 at 15:26):

You are suggesting to "add a dummy Obj.magic cast at application time". What I am saying is that there should not even be an application in nativevalues.ml. So, we don't even need this workaround.

Pierre-Marie Pédrot (Apr 20 2022 at 15:29):

I'm not sure I understand?

Guillaume Melquiond (Apr 20 2022 at 15:30):

I am saying that we can directly remove type t = t -> t from nativevalues.ml.

Pierre-Marie Pédrot (Apr 20 2022 at 15:30):

no you can't

Pierre-Marie Pédrot (Apr 20 2022 at 15:30):

this will break the native compiler scheme, you'll get type errors at OCaml compilation time of native files

Guillaume Melquiond (Apr 20 2022 at 15:30):

Which code in this file requires the type to be recursive rather than just abstract?

Pierre-Marie Pédrot (Apr 20 2022 at 15:31):

none in this file, but it's part of the public API of the native compiler

Pierre-Marie Pédrot (Apr 20 2022 at 15:31):

you have to change the compilation scheme of miniML

Guillaume Melquiond (Apr 20 2022 at 15:31):

My point is that it does not have to be part of the public API. Only the generated files care about t being recursive. Coq itself does not care.

Pierre-Marie Pédrot (Apr 20 2022 at 15:31):

This, I agree with. But once again it's more tricky than it seems

Pierre-Marie Pédrot (Apr 20 2022 at 15:32):

I mean, it's not undoable, but it's not trivial either

Pierre-Marie Pédrot (Apr 20 2022 at 15:33):

so in the current implementation if you remove this transparent equirec definition, it'd break every call to native compute

Gaëtan Gilbert (Apr 20 2022 at 21:07):

when are we moving native compute to something that doesn't interact with the ocaml typer?

Gaëtan Gilbert (Apr 20 2022 at 21:12):

PS logic_monad is also doing something tricky with rectypes in its implementation

Pierre-Marie Pédrot (Apr 20 2022 at 21:13):

@Gaëtan Gilbert depending on the amount of non-interaction this ranges from ~ a week of work to ~ a complete rehauling of the system

Pierre-Marie Pédrot (Apr 20 2022 at 21:14):

I've been advocating for another target language (namely, malfunction) but this also has its share of hurdles

Pierre-Marie Pédrot (Apr 22 2022 at 11:10):

I've rebased and cleaned up my old POC branch to remove the native value equirec type, it seems to work properly.

Pierre-Marie Pédrot (Apr 22 2022 at 11:10):

I'll submit it soon.

Maxime Dénès (Apr 25 2022 at 06:52):

Can you remind us what the motivation is for removing -rectypes? I'm surprised this has become a priority, TBH.

Maxime Dénès (Apr 25 2022 at 06:53):

Other question: is the generated code still readable or are there calls to Obj.magic everywhere in practice?

Guillaume Melquiond (Apr 25 2022 at 06:57):

(I would not call it a priority.) The reason is that the code extracted by extraction/ExtrOCamlInt63.v relies on kernel/uint63.ml, which is compiled with -rectypes. This makes it painful for people to link their extracted code. They have to ship their own copy of kernel/uint63.ml.

Guillaume Melquiond (Apr 25 2022 at 06:59):

More generally, this would hit anyone trying to build a wrapper around Coq rather than just a plugin.

Karl Palmskog (Apr 25 2022 at 06:59):

see: https://github.com/coq/coq/issues/15936

Pierre-Marie Pédrot (Apr 25 2022 at 07:16):

I am also not happy with -rectypes from a dev point of view. It is a contaminating flag that results in horrible typing errors.

Pierre-Marie Pédrot (Apr 25 2022 at 07:17):

Not unbearable but quite annoying at times.

Gaëtan Gilbert (Apr 25 2022 at 09:27):

we also get the occasional -rectypes-only ocaml bug

Jacques Garrigue (Apr 25 2022 at 09:43):

Honestly, if you can get rid of it this is a good thing.
Outside of backward compatibility (never remove a feature), the only reasons -rectypes is there is for generated code (useful for synchronous languages for instance), and to let people experiment.
By the way, where does the need for -rectypes stem from?

Pierre-Marie Pédrot (Apr 25 2022 at 09:44):

@Jacques Garrigue cf the beginning of the thread

Gaëtan Gilbert (Apr 25 2022 at 09:44):

By the way, where does the need for -rectypes stem from?

generated code ('native compile')
also a few minor uses only in implementations

Jacques Garrigue (Apr 25 2022 at 09:46):

Sorry, not used to Zulip yet.

Jacques Garrigue (Apr 25 2022 at 10:45):

I read the discussion. If the main problem is the t = t -> t equation, you might want to try introducing a local equation through a GADT.
Suppose that t is defined somewhere:

module M = struct
  type t
  type (_,_) eq = Refl : ('a,'a) eq
  let eqn : (t, t -> t) eq = Obj.magic ()
end

and then add

open M
let Refl  = eqn in ...

wherever you want to use the equation.
For instance:

let Refl = eqn in (fun x -> x : t)

You don't even need to use -rectypes.
The only drawback is that you currently cannot add the equation for the whole file, but only for individual expressions.

Gaëtan Gilbert (Apr 25 2022 at 10:48):

it's more (fun (x:t) y z -> x y z) though

Jacques Garrigue (Apr 25 2022 at 10:50):

let f = let Refl = eqn in (fun (x:t) (y:t) (z:t) -> x y z : t)

Gaëtan Gilbert (Apr 25 2022 at 10:51):

that's a lot of annotation

Jacques Garrigue (Apr 25 2022 at 11:04):

If there is only one type, you just put the same annotation everywhere.

Pierre-Marie Pédrot (Apr 25 2022 at 12:34):

Nah, the nativevalue problem is really a non-issue from the typing point of view.

Pierre-Marie Pédrot (Apr 25 2022 at 12:34):

we would like to target an untyped OCaml but there is no such thing

Pierre-Marie Pédrot (Apr 25 2022 at 13:44):

https://github.com/coq/coq/pull/15944

Last updated: Oct 08 2024 at 15:02 UTC