Question about function syntax

Stream: new members

[R Dong]

Hello, I am following the Functional Programming in Lean book. While I have a lot of experience with other FP languages, proof assistants are something new to me, and I think I am not fully understanding the syntax of the language.

Are all of the following actually the same type? I see that the book sometimes name the arguments, sometimes not. I am not sure when is each choice being made.

def f (a : Nat) : Nat -> Nat := sorry
#print f

def g (a : Nat) (b : Nat) : Nat := sorry
#print g

def Nat.h (a : Nat) : Nat -> Nat := sorry
#print Nat.h

Also, I don't know when is the dot notation allowed. For instance, 0.h does not seem to be valid, nor is x.h if x is defined as a Nat. However, the following seems to be OK:

def p (a : Nat) : Nat -> Nat := a.h

What are the actual rules for the dot notation? Do they work only for bound variables?

Also, when can I use the "guard" syntax? Are the following equivalent?

def fs (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | _::_ => 1

def gs : List α -> Nat
  | [] => 0
  | _::_ => 1

def hs : (xs : List α) -> Nat
  | [] => 0
  | _::_ => 1

And why would I pick one over the other, except for deciding on if a name is needed?

Thank you.

[Kevin Buzzard]

Are all of the following actually the same type?

You can just ask Lean:

#check f = g -- no error
#check g = Nat.h -- no error

These commands succeed so f,g,Nat.h must have the same type, as f = g would not typecheck if their types were different.

The reason 0.h is not valid mustmight be something to do with the order in which things are elaborated. The issue is that 0 is an ambiguous term; any type X with an instance of [Zero X] will have 0 : X. However (0 : Nat).h is fine. I can't reproduce your claim that x.h doesn't work:

variable (x : Nat) in
#check x.h -- works fine

so maybe the rules are what you think they are, and you just got caught out by unrelated stuff. I'll let others comment on "guard" as I don't really know what the word means.

[Ruben Van de Velde]

I think with 0.h there might also be confusion with parsing floats

[Kevin Buzzard]

In that case I'll tone down my claim about it :-)

[R Dong]

If I do this:

def Nat.h (x : Nat) : Nat := sorry
def x : Nat := 0
#print x.h

I get an error unknown constant 'x.h'

[Derek Rhodes]

Hi @R Dong, using #eval instead of #print provides a clue:

cannot evaluate expression that depends on the sorry axiom. Use #eval! to evaluate nevertheless (which may cause lean to crash).

def Nat.h (x : Nat) : Nat := sorry
def x : Nat := 0
#check x.h
#eval x.h

[R Dong]

Oh, I see. I thought it would just throw an exception or something.