How to understand delimiters used in Lean structures?

Stream: new members

[Noah Stebbins]

Hi guys, I'm trying to develop intuition for why this code works the way it does.

universe u v

structure MyStruct where
    {α : Type u}
    {β : Type v}
    a : α
    b : β

structure MyStruct2 (α: Type u)(β: Type v) where
    a : α
    b : β

structure MyStruct3 (α: Type u) where
  a : α
  b : α

#check { a := 10, b := true : MyStruct }
#check { a := 10, b := true : MyStruct2 } -- type-related error
#check { a := 10, b := true : MyStruct2 Nat Bool }
#check { a := 10, b := 11 : MyStruct3 Nat }

As a newbie to Lean, I get very confused by which delimiters to use and where. Why is MyStruct cool without explicit type arguments and why does it work if you provide them? And in this case why are there multiple ways for defining essentially the same structure?

It's worth noting that my background is Java and Python where you essentially only specify one place for 'arguments'. And for Java Generics, afaik there's only one place within a class definition to put the Generic type parameter T.

So while I love playing around with Lean's tactics, I have found Lean's delimiters for things like inductive types and structures confusing.

[Bolton Bailey]

Why is MyStruct cool without explicit type arguments

I guess that the reason that the Lean language designers chose this is for the same reason there are implicit arguments to functions - it makes it faster to express values of this type.

and why does it work if you provide them?

I guess you are asking why

#check { α := Nat, β := Bool, a := 10, b := true : MyStruct }

works? I guess when all these values are referred to by their label in the definition, there is no ambiguity.

And in this case why are there multiple ways for defining essentially the same structure?

MyStruct, MyStruct2, MyStruct3 are different structures, the first is just essentially a 4-tuple consisting of 2 types and two terms one from each of the types. MyStruct2 by contrast is a function which takes 2 types as arguments.

[Markus Schmaus]

If by "delimiters" you mean the curly braces, the Lean manual on implicit arugments is probably useful reading. An implicit argument is an argument with a special kind of default value, namely whatever makes this code type check.

Maybe this is also helpful:

universe u v

structure MyStruct where
    {α : Type u}
    {β : Type v}
    a : α
    b : β

structure MyStruct2 (α: Type u)(β: Type v) where
    a : α
    b : β

structure MyStruct4 {α: Type u}{β: Type v} where
    a : α
    b : β


#check { a := 10, b := true : MyStruct } -- works because α and β are implicit
#check { a := 10, b := true : MyStruct2 } -- doens't work because the explicit arguments α and β are missing
#check { a := 10, b := true : MyStruct2 _ _ } -- works because the explicit arguments are given as wildcards and Lean can figure them out
#check { a := 10, b := true : MyStruct4 } -- works because α and β are implicit

[Noah Stebbins]

Thank you for the help!

[Daniel Weber]

You should note that MyStruct and MyStruct4 are different:

structure MyStruct where
    {α : Type u}
    {β : Type v}
    a : α
    b : β

structure MyStruct4 {α: Type u} {β: Type v} where
    a : α
    b : β


#check { a := 10, b := true : MyStruct }.α -- works because α is part of the structure
#check { a := 10, b := true : MyStruct4 }.α -- doesn't work because α is part of the type of the structure

[Noah Stebbins]

This community’s ability to be encouraging and give comprehensive answers impresses me