Stream: Coq devs & plugin devs

Topic: Why do we use -rectypes?


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

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 14:44):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 14:45):

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

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

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

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

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

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

view this post on Zulip Ali Caglayan (Apr 20 2022 at 14:56):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 14:56):

Which type is that?

view this post on Zulip Ali Caglayan (Apr 20 2022 at 14:57):

ln 1032

view this post on Zulip Ali Caglayan (Apr 20 2022 at 14:57):

State.t

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 14:57):

Oh, yes, you could box that one.

view this post on Zulip Ali Caglayan (Apr 20 2022 at 14:59):

What is your suggestion for constr?

view this post on Zulip Ali Caglayan (Apr 20 2022 at 15:00):

Just inline "constr" everywhere?

view this post on Zulip Ali Caglayan (Apr 20 2022 at 15:01):

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 15:22):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 15:22):

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 15:29):

I'm not sure I understand?

view this post on Zulip Guillaume Melquiond (Apr 20 2022 at 15:30):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 15:30):

no you can't

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

view this post on Zulip Guillaume Melquiond (Apr 20 2022 at 15:30):

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 15:31):

you have to change the compilation scheme of miniML

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 15:31):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2022 at 15:32):

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

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

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

view this post on Zulip Gaëtan Gilbert (Apr 20 2022 at 21:12):

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

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 22 2022 at 11:10):

I'll submit it soon.

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

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

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

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

view this post on Zulip Karl Palmskog (Apr 25 2022 at 06:59):

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 25 2022 at 07:17):

Not unbearable but quite annoying at times.

view this post on Zulip Gaëtan Gilbert (Apr 25 2022 at 09:27):

we also get the occasional -rectypes-only ocaml bug

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

view this post on Zulip Pierre-Marie Pédrot (Apr 25 2022 at 09:44):

@Jacques Garrigue cf the beginning of the thread

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

view this post on Zulip Jacques Garrigue (Apr 25 2022 at 09:46):

Sorry, not used to Zulip yet.

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

view this post on Zulip Gaëtan Gilbert (Apr 25 2022 at 10:48):

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

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

view this post on Zulip Gaëtan Gilbert (Apr 25 2022 at 10:51):

that's a lot of annotation

view this post on Zulip Jacques Garrigue (Apr 25 2022 at 11:04):

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

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

view this post on Zulip Pierre-Marie Pédrot (Apr 25 2022 at 12:34):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 25 2022 at 13:44):

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


Last updated: Feb 06 2023 at 00:03 UTC