What is the difference between this?

Stream: new members

[ptrl]

I am a new learner of lean4, following this tutorial. And I have some question about:

axiom and_comm (p q : Prop) : Proof (Implies (And p q) (And q p))
axiom and_comm2 : (p q : Prop) -> Proof (Implies (And p q) (And q p))
#check and_comm
#check and_comm2

and_comm and and_comm2 look definitely same and here question comes:
Why I cannot write like this:

def double (x : Nat) : Nat := x + x
def double2 : (x : Nat) -> Nat := x + x -- unknown identifier 'x'

[Eric Wieser]

You have to write def double2 : (x : Nat) -> Nat := fun x => x + x

[ptrl]

Eric Wieser said:

You have to write def double2 : (x : Nat) -> Nat := fun x => x + x

Why I can use x in double but I cannot use x in double2?
They look same.
Maybe there are some special rule on pattern like def double(x: Nat) : Nat rather than def double2 : (x: Nat) -> Nat?

[Jeremy Tan]

double2, by its type definition (x : Nat) -> Nat making it a function, should return a function Nat -> Nat instead of just Nat

[ptrl]

Oh, thank you so much. I understand.

[Jeremy Tan]

Lean 4 is the world's most strongly typed programming language. So strong that proofs are themselves types and unification is a grand mess

[Eric Wieser]

ptrl said:

Why I can use x in double but I cannot use x in double2?

because putting (x) before the colon is shorthand for writing fun x =>

[Eric Wieser]

Try looking at #print double and #print double2 to see what's going on

[Kevin Buzzard]

Lean 4 is very strongly typed, but I would be careful about believing comments from someone who has only been using the system for about a week :-)

[Eric Wieser]

(Kevin is referring to Jeremy, not me :))

[Kevin Buzzard]

The correct comment is that lean 4 is very strongly typed and also takes more than a week to get the hang of it.

[Martin Dvořák]

Jeremy Tan said:

Lean 4 is the world's most strongly typed programming language. So strong that proofs are themselves types and unification is a grand mess

I agree with the first part. Lean 4 is indeed very strongly typed.

I don't think the second part is correct. Afaik, proofs are terms, propositions are types. We could also say that propositions are terms. I don't think, however, that proofs are types.

[Mario Carneiro]

It's also not the world's strongest type system. An important type system feature you won't find in lean is substructural / affine types; the most popular language today with affine typing is Rust, although Haskell also has some linear types in a GHC extension

[Mario Carneiro]

intersection types and refinement types are also not present in lean

[Mario Carneiro]

(That is not to say that it is necessarily desirable to add every type system feature under the sun into lean. The stronger the type system, the harder it gets to perform type checking, and if it becomes undecidable then the user has to intercede sometimes and you end up with another kind of tactic system.)

[Reid Barton]

Also, for people trying to prove ordinary mathematical theorems, it might be unclear what the meanings of the new fancy types are.

[Martin Dvořák]

Mario Carneiro said:

intersection types and refinement types are also not present in lean

Why doesn't subtyping in Lean qualify as refinement types?