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.

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.

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).`

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

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?

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

Last updated: Oct 13 2024 at 01:02 UTC