what "purely functional" means?

Stream: new members

[Asei Inoue]

I’m a beginner, and I might be making a silly mistake, so I’d like to confirm what the term “purely functional language” really means.

Consider the division function Nat.div, which is defined with the type Nat → Nat → Nat.
Would it be correct to explain it as follows?
“Since the function is defined with the type Nat → Nat → Nat, and Lean is a purely functional language, it is only allowed to return a term of type Nat. Therefore, returning a division-by-zero error is not permitted.”

I suspect that this explanation might be incorrect.
I think that “a function that terminates and returns a value for every argument in its domain” is a matter of totality, which is a different concept from purity.
However, I’m not very confident about this.

I’d appreciate it if you could clarify this for me.

[Henrik Böving]

The term means if you call a function f with a value x twice the result of both calls is always the same.

[Arthur Paulino]

What I understand as "purely functional" is that it's more like lambda calculus than a Turing machine.

In languages like C and Rust, you have direct stateful control of the machine's memory. But in Lean and Haskell, the notion of state is built with abstractions on top of fundamentally stateless blocks.

[Arthur Paulino]

Henrik Böving said:

The term means if you call a function f with a value x twice the result of both calls is always the same.

Isn't this a bit tricky for e.g. functions in StateM?

[Kenny Lau]

the results are still the same, but the results in turn is a function of the state

[Kenny Lau]

you're describing how monads are possible

[Henrik Böving]

Arthur Paulino said:

Henrik Böving said:

The term means if you call a function f with a value x twice the result of both calls is always the same.

Isn't this a bit tricky for e.g. functions in StateM?

No, f : StateM s Unit is an alias for f : s -> (s x Unit) so you are passing in a state parameter. Same thing for IO where you are passing in the real world parameter.

[Arthur Paulino]

Makes sense! Though this is what I meant by "a bit tricky". One needs to understand how the notion of state is realized in a monadic context

[Kenny Lau]

this seems like an unnecessary distraction for a "beginner"

[Arthur Paulino]

Hmm, questionable. This is precisely what confused me when I was a beginner because when I looked at slightly more involved Lean code it often used stateful monads.

[Kenny Lau]

which part of the library were you looking at?

[Asei Inoue]

“Since the function is defined with the type Nat → Nat → Nat, and Lean is a purely functional language, it is only allowed to return a term of type Nat. Therefore, returning a division-by-zero error is not permitted.”

So, is this explanation wrong? Or is it correct? I still don’t know.

[Arthur Paulino]

Kenny Lau said:

which part of the library were you looking at?

The metaprogramming API.

@Asei Inoue it can't return anything else besides Nat because it wouldn't typecheck otherwise.

Take Python, for example. You can have a division function that takes two numbers and has the result based on some global variable, which dictates the behavior of the function when the divisor is zero. Even if this function is type-consistent, it's still not purely functional.

[Kenny Lau]

Arthur Paulino said:

The metaprogramming API.

right, ofc if you want to go into metaprogramming then you would have to learn about monads, but 99% of the mathlib users are there to do maths

[Alex Meiburg]

I think that sentence you quoted is alluding to a certain model of error handling, a model you see in many imperative languages. In Java, you could have a int f(int x, int y), which "should" always return an integer. But there's also a massive global state, which any function can modify. Part of that global state is, you could say, a big stack of callers. So the function is free to, instead of returning normally, throw an exception - which then searches up the stack for the appropriate error handler to jump to instead.

That's a very not-pure kind of action, to look at and act upon global state like that. A purely functional setting wouldn't allow such error-handling jumps.

[Kenny Lau]

Asei Inoue said:

I think that “a function that terminates and returns a value for every argument in its domain” is a matter of totality, which is a different concept from purity.

termination is an entirely different concept, in Lean functions are allowed to not terminate, but they still typecheck

[Kenny Lau]

now if you actually write a non-terminating function, Lean will detect that and force you to put noncomputable before the definition

[Alex Meiburg]

^^ but remember that, if you're coming from an imperative background, totality is also entirely unrelated to termination - so treating those two as equivalent could be very confusing!

[Kenny Lau]

let's say that without assuming termination, a function _ -> Nat has to theoretically return a natural number, even after infinitely many steps

[Riccardo Brasca]

Isn't "purely functional" related to the fact that the only thing Lean does when executing a program is evaluating functions? For example there is no "for cycle" (we can simulate it of course, but i++ is meaningless).

[Aaron Liu]

to me "purely functional" mean that everything is immutable (in theory)

[Aaron Liu]

A consequence of this is that, if you run the same function twice with the same inputs, since nothing has mutated between the function calls, it should give the same result

[Alex Meiburg]

giving the same result is one aspect (not 'reading' from a global state), but also it shouldn't 'write' to any kind of global state. x = f 37; y = f 37; return y should be equivalent code to return f 37

[Henrik Böving]

As long as the global state is write only it shouldn't matter should it^^

[Alfredo Moreira-Rosa]

Asei Inoue said:
So, is this explanation wrong? Or is it correct? I still don’t know.**

[Alfredo Moreira-Rosa]

The explanation is wrong. A pure function can return an error as long as any change of the evironment don't change the resulting error and that itself don't change the environment.
To take your example, a function that does division can return an Option (or an Except) that is none (or error) when dividing by zero and it's still a pure function.
Like @Henrik Böving said, a pure function is a function that always return the same result given the same input.
Why lean returns 0 for a division by 0 and not terminate the program is more to have a total function for mathematical properties.
But this also makes it a pure function.

[Rado Kirov]

Somewhat related I wrote a blog post about "pure functions" in JS - https://rkirov.github.io/posts/pure/