Are Global Variables OK?

Stream: new members

[James B Clifford]

I'm new to functional programming and I come from a C# background. I just wrote my first program in F# and I ended up putting the meat of my program in a class with a bunch of mutable members. I know I just mentioned F# but I am trying to learn lean, and functional programming along the way. Anyway, my question is, if I am writing a program that operates on an object, like a graph, and all the operations on that graph return a new graph, should I keep a variable that points to the current graph in global scope?

[Eric Wieser]

What do you mean by a "global variable" in Lean? Are you using Lean3 or Lean4?

[James B Clifford]

lean4. In OOP global variables are discouraged. But they appear to be OK here. I'm just trying to verify , or ask If I'm missing something.

[Patrick Massot]

You missed the first question, which was very important.

[Patrick Massot]

You will have a lot to unlearn, but this is part of the fun of switching to another programming paradigm!

[Gareth Ma]

Showing maybe a code snippet explaining "In OOP global variables are discouraged. But they appear to be OK here" will help.

[Patrick Massot]

At least in a simplified form, the final answer is probably: global variables in your sense don't exist at all in Lean 4.

[Eric Wieser]

With the follow up answer of "variables (x : Nat) is not declaring a global variable, it's declaring function arguments"

[James B Clifford]

so you mean to tell me that there is no concept of scope in lean4?

[Eric Wieser]

There's no concept of global scope

[Eric Wieser]

The closest you can reasonably get is the docs4#StateM monad which lets you implicitly thread a piece of state through a call stack

[Tomas Skrivan]

I think global mutable variable is more like IO.Ref and it is as bad as in other programming languages. You should think twice before using it.