[waltpad]

Sorry, I got confused on the meaning linear.

As explained in the other answer, it's possible to implement the power function which is "type-linear" on each argument, but that function will not otherwise be linear (ie, the mathematical meaning of linear) on its arguments.

In Rust for instance, affine types are used to restrict usage of values linearly, which means that a value passed as argument will be by default moved from caller to callee: The value will not be available anymore to the caller. This has some consequences for instance for binary operators on values which require special care when moved (structures, arrays): with the restriction explained above, a value cannot be passed more than once to a function, and thus doing something like 'mult(x,x)' (where x is eg. a matrix) will not work because x appears twice, but may only be moved once. The solution offered by the language, called "borrowing" is to use references for the arguments: a borrowed value is no longer being moved; instead, it remains in the scope of the caller, and the callee only receives a reference. References may be created and duplicated, allowing multiple uses of the same piece of data.

[goldenkey]

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]

Well, 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]

I 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.