21 ms·
Forgive me but if we actually have to implement mathematics from pure computational theory, wouldn't type-linear functions be equivalent to actual mathematical
by goldenkey 6y ago
Forgive me but if we actually have to implement mathematics from pure computational theory, wouldn't type-linear functions be equivalent to actual mathematical linear functions?
- waltpad 6y agoWell, if copies may be borrowed, as it is the case in Rust, I suppose that a type-linear function, as I called it, doesn't have to be computationally linear. The `mult` example we discussed could not be applied twice to the same value, unless it is declared as borrowing its parameters from the caller. Elaborating on this, with a function signature like the following: fn mult(x : Vec<f32>, y : Vec<f32>) -> Vec<f32> { // matrix product implementation } arguments x and y cannot point to the same value, because a value cannot be moved twice. A call like mult(a,a) will generate an error. Conversely, with the following signature: fn mult(x : &Vec<f32>, y : &Vec<f32>) -> Vec<f32> { // ... } the call: mult(&a,&a) will typecheck, because values are passed by reference. Now, nothing prevents one to implement the function square, based on the second version of mult: fn square(x : Vec<f32>) -> Vec<f32> { return mult(&x,&x) } which is type-linear on its parameter x, but computationally is not linear. Clearly your original question was spot on.
- goldenkey 6y agoI see what you mean with the copying. I just thought based on OPs comments there would have been a strong correspondence between lambda calculus numbers (Church encoding) and the operations on them, and actual type-linear functions.