## Stream: new members

### Topic: constants and variables

#### Patrick Thomas (Mar 25 2019 at 02:55):

Is scoping the only difference between constants and variables in Lean?

#### Kenny Lau (Mar 25 2019 at 02:57):

constants are axioms while variables is just a shorthand to insert "forall" in the following theorems

#### Kenny Lau (Mar 25 2019 at 02:57):

so for example classical.choice is a constant

#### Patrick Thomas (Mar 25 2019 at 03:00):

"forall" as an assumed hypothesis in all the following theorems?

#### Patrick Thomas (Mar 25 2019 at 03:02):

I guess I'm not certain how that differs from an axiom.

#### Kenny Lau (Mar 25 2019 at 03:05):

I have struggled explaining it before, but I guess I'll still try

#### Mario Carneiro (Mar 25 2019 at 03:06):

constant never goes out of scope, it's as permanent as a def

#### Kenny Lau (Mar 25 2019 at 03:06):

def f : nat -> nat := fun x, x+1 is the same as:

variable (n : nat)
def f : nat := n + 1


#### Kenny Lau (Mar 25 2019 at 03:07):

but if you do:

constant n : nat
def g : nat := n + 1


then you're declaring a constant n and g is now a natural number, not a function

#### Kenny Lau (Mar 25 2019 at 03:07):

f 3 evaluates to 4 while g 3 is a type mismatch because the type of g is nat

#### Mario Carneiro (Mar 25 2019 at 03:08):

f (f n) works but g (g n) doesn't make sense

#### Kenny Lau (Mar 25 2019 at 03:08):

g n doesn't make sense to start with?

#### Mario Carneiro (Mar 25 2019 at 03:09):

My point being that there is no analog of f (f n) for g

#### Mario Carneiro (Mar 25 2019 at 03:09):

you can't substitute for a constant

#### Patrick Thomas (Mar 25 2019 at 03:16):

So it is like constants and variables in C? I.e. const float pi = 3.14, versus int x = 0. pi can never take a different value, but x can?

#### Kenny Lau (Mar 25 2019 at 03:18):

well Lean is a functional programming language like Haskell, unlike the more conventional programming languages (C, Java, Python) which are imperative languages

#### Kenny Lau (Mar 25 2019 at 03:18):

but Lean constant would be C const with a "secret" value

#### Kenny Lau (Mar 25 2019 at 03:18):

where variable is just the input to functions

#### Patrick Thomas (Mar 25 2019 at 03:28):

I think I kind of see. I started reading a tutorial on Haskell earlier this week. Does it have something similar that I will run across?

#### Kenny Lau (Mar 25 2019 at 03:30):

I don't know Haskell but I don't think so

#### Patrick Thomas (Mar 25 2019 at 03:37):

Is a variable the same as a variable in the lambda calculus?

yes

#### Patrick Thomas (Mar 25 2019 at 03:39):

Ah. I have not gotten to the typed lambda calculus yet. Will I see constants there?

#### Mario Carneiro (Mar 25 2019 at 03:41):

Constants are like Haskell compiler intrinsic functions

#### Mario Carneiro (Mar 25 2019 at 03:42):

they are functions, you can see that they have been declared as such, but you can't see the definition

#### Mario Carneiro (Mar 25 2019 at 03:45):

Haskell doesn't really have an equivalent to the variables command. Scopes are handled differently in Haskell - you can think of the whole program as being in a single shared scopes where all your definitions are like let bindings. Lean is not like that - there are no variable scopes that span multiple definitions

#### Patrick Thomas (Mar 25 2019 at 03:48):

I guess I haven't gotten that far yet.

#### Patrick Thomas (Mar 25 2019 at 03:49):

Are constants the same as the "term constants" mentioned here: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

yes

Thank you

#### Kevin Buzzard (Mar 25 2019 at 07:08):

One other difference is that users are hugely discouraged from ever using constants ever. I'm not sure there's a single one in mathlib. But there are variables everywhere

Last updated: May 11 2021 at 00:31 UTC