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