I was told that Rust has a semantics in affine logic -- so one has deletion/weakening but not duplication/contraction.
The following compiles:
fn throw_away<A, B>(x: A, _y: B) -> A {
x
}
Because duplication is disallowed, the following does not compile:
fn dup<A>(x: A) -> (A, A) {
(x, x)
}
Similarly, neither of these compile:
fn throw_away3<A, B>(x: A, f: fn(A) -> B) -> A {
x;
f(x)
}
fn throw_away4<A, B>(x: A, f: fn(A) -> B) -> A {
throw_away(x, f(x))
}
Weakening is also witnessable
fn weaken<A, B, C>(f: fn(A) -> B) -> impl Fn(A, C) -> B {
move |x: A, y: C| f(x)
}
Instead of returning fn(A, C) -> B, we returned impl Fn(A, C) -> B. Is there a way to return fn(A, C) -> B instead? It's fine if not; I'm just curious.
Something else I expect is that you can lift A to () -> A. However, functions in Rust can be duplicated and used more than once. For example,
fn app_twice(f: fn(A) -> A, x: A) -> A {
f(f(x))
}
Suppose there was actually a function lift(x: A) -> fn() -> A, then we could break the move semantics. For example, this would allow
fn dup_allowed(x: A) -> (A, A) {
let h = lift(x);
(h(), h())
}
Thus to lift A to fn() -> A, we need to know that the function is "linear/affine" or can be used only once. Rust provides a type for this: FnOnce() -> A. In the following, the first compiles, and the second does not.
fn app_once(f: impl FnOnce(A) -> A, x: A) -> A {
f(x)
}
fn app_twice2(f: impl FnOnce(A) -> A, x: A) -> A {
f(f(x))
}
The following functions are inverses of each other (probably, I don't know Rust's semantics well enough to say that they are actually inverse to each other):
fn lift_up<A>(x: A) -> impl FnOnce() -> A {
move || x
}
fn lift_up_r<A>(f: impl FnOnce() -> A) -> A {
f()
}
Since fn dup<A>(x: A) -> (A, A) { (x,x) } does not compile, I thought that the following might be a problem:
fn dup<A>(x: fn() -> A) -> (A, A) {
(x(), x())
}
It seems that Rust is doing something special for fn(A) -> B types.
Why don't I have to declare that x is reusable/duplicable in the above?
Perhaps something different is going on. Declared functions are a bit special fn f(x: A) -> B { ... } is a particular witness that A -> B. Thus if f needs to be used multiple times, it can be reproved as many times as needed, but fn(A) -> B is a completely different thing: it is not a constructed thing but a hypothetical thing, and must be using that fn(A) -> Bs are duplicatable. In fact, I've been thinking that it's more like a freely duplicable entity. Here's my rough analogy:
fn my_fun<A,B>(x :A) -> B { M }"is" x:A |- M:Bfn(A) -> B"is" !(A -o B) hence freely duplicable- Thus
fn() -> A"is" !(() -o A) = !A hencefn () -> Ais the (co)free duplication on A fn dup_arg<A: Copy>(x: A) -> B { M }"says" that A has duplication or is a comonoidimpl FnOnce (A) -> B"is" A -o B
But this can't be right... For what is impl Fn(A) -> B? From playing around a bit, it seems that fn(A) -> B is more strict than Fn(A) -> B. What am I missing?