Stream: Coq devs & plugin devs

Topic: Advice regarding extraction to rust


view this post on Zulip walker (Aug 07 2022 at 17:14):

So I am doing test driven dev here and I am to some degree stuck at extracting from something like this:

Definition test2 (f:nat -> nat -> nat) (x:nat):= f x.

This generate MiniML ast that looks as follows

{
  "what": "decl:term", "name": "test2",
  "type": {
    "what": "type:arrow",
    "left": {
      "what": "type:arrow",
      "left": {
        "what": "type:glob", "name": "nat", "args": [

        ]
      },
      "right": {
        "what": "type:arrow",
        "left": {
          "what": "type:glob", "name": "nat", "args": [

          ]
        }, "right": {
          "what": "type:glob", "name": "nat", "args": [

          ]
        }
      }
    },
    "right": {
      "what": "type:arrow",
      "left": {
        "what": "type:glob", "name": "nat", "args": [

        ]
      },
      "right": {
        "what": "type:arrow",
        "left": {
          "what": "type:glob", "name": "nat", "args": [

          ]
        }, "right": {
          "what": "type:glob", "name": "nat", "args": [

          ]
        }
      }
    }
  },
  "value": {
    "what": "expr:lambda", "argnames": [
      "f"
    ], "body": {
      "what": "expr:rel", "name": "f"
    }
  }
}

Note that the variable X is gone,

In Ocaml I understand this is easy to represent as follows:

let test2 f = f

. but in Rust it is not.
The best I can get without complex tricks is

fn test2 (f : impl Fn (nat) -> nat, x: nat) nat {
    f x
}

So My question here is two folds,
I there a good way to stop MiniML engine from performing this specific optimization
B- If not how can I safely generate unused variable name & how can I go transform the unwanted AST case (in ocaml) into the one I desire systematically.

view this post on Zulip walker (Aug 07 2022 at 17:15):

In this particular case it is trivial to do, but I am worried about bugs with partially applied functions with many arguments, so Iam looking for the cleanest possible solution.

view this post on Zulip Gaëtan Gilbert (Aug 07 2022 at 18:54):

I guess this is related to the first 2 bullet points in https://www.irif.fr/~letouzey/scheme/
so eg you need to think about what you would produce for Definition bla f : nat := f (test2 plus).

view this post on Zulip walker (Aug 07 2022 at 19:58):

It feels like tirival but when I try to implement it feels less trivial.

view this post on Zulip Pierre-Marie Pédrot (Aug 07 2022 at 20:55):

Note that the OCaml runtime does this kind of dynamic dispatch on arity under the curtains. I don't think it's as easy to do in Rust without wreaking havoc with the type system, since closures are not first-class. You'll likely also face trouble with monomorphisation, so you'll have to box everything. Is it actually known that the Rust type system can embed MiniML?

view this post on Zulip walker (Aug 08 2022 at 05:32):

probably not, but I thought maybe there is way to do inefficient transpiling


Last updated: Feb 02 2023 at 15:04 UTC