anonymous structure types

Stream: lean4

[Anders Christiansen Sørby]

Is it possible do define anonymous structure type syntax with the current system?
For example

structure Any := (type : Type ) (val : type)
inductive Struct | MyCons {a: A, b : B}
-- And
def f : Struct -> Any
  | MyCons { a, b} => {val := a, type := A}

Which is closer to Haskell syntax.

[Mario Carneiro]

You can do this:

structure Any := (type : Type ) (val : type)
inductive Struct | mk (a: A) (b : B) : Struct

def f : Struct -> Any
  | ⟨a, b⟩ => {val := a, type := _}

[Mario Carneiro]

I don't see why we should support multiple syntaxes for the same thing, beyond what lean already supports vis-a-vis moving arguments across the colon and structure / inductive

[Leonardo de Moura]

Here are other alternatives:

structure Any where
  type : Type
  val  : type

structure Struct where
   myCons :: -- You can give your own name to the structure constructor
     a : Nat
     b : Bool

def f₁ : Struct -> Any
  | { a, b } => { val := a } -- We don't need to provide `type`

def f₂ : Struct -> Any
  | .myCons a b => { val := a } -- The namespace at `.myCons` is inferred by Lean

def f₃ : Struct -> Any
  | Struct.myCons a b => { val := a }

inductive Struct' where
  | myCons (a : Nat) (b : Bool)

-- You cannot use the structure instance notation with inductive datatypes
-- even if they have only one constructor
-- def f₄ : Struct' -> Any
--  | { a, b } => { val := a }

def f₅ : Struct' -> Any
  | .myCons a b => { val := a }

def f₆ : Struct' -> Any
  | Struct'.myCons a b => { val := a }

[Anders Christiansen Sørby]

Why doesn't this work:

structure Struct where
   myCons ::
     a : Nat
     b : Bool
  myOtherCons ::
     a : Nat
     b : Bool

Would be really nice to do this. Rust and Haskell supports it.

[Sebastian Ullrich]

The point of a structure is that is has exactly one constructor, and this is true in Rust and Haskell as well. Basically all the special syntax for structures is dependent on this property. I assume you you are referring to struct-like enums in Rust; I'm not sure what you're referring to in Haskell. It's always a good idea to make these things explicit in a proposal, and in particular to mention actual advantages and use cases.

[Anders Christiansen Sørby]

Yes. I'm thinking of the struct like enums in rust (I guess haskell only has them for single constructors). So my suggestion would be something like

inductive EnumStruct | myCons {a: A, b : B} | myOtherCons {a : A, c: C}
open
def m : EnumStruct -> A
 | .myCons { a, b } => a
 | .myOtherCons { a, c } => a

But another use of anonymous structure types could be to pattern match select a class of structures that has some particular fields

structure SA :=
  a : A
  b : B

structure SB :=
  a : A
 c : C

-- Which would implicitly define a class something like this
-- Which is a Lens I guess
class HasField (name: Name) (F : Type) (A : Type) where
  getField : A -> F
  putField : A -> F -> A

instance : HasField (@a) A SA := -- SA.a ...
instance : HasField (@a) A SB := -- SB.a ...

-- which can then be used as a normal structure type
def act (s : { a : A }) : A := s.a

This could be a part of adding Lenses and optics if that is something you are looking into.

[Sebastian Ullrich]

I'm not sure if HasField makes sense in Lean. We don't have global field names like in Haskell.

[Sebastian Ullrich]

And Lean is a completely nominal language like Rust and Haskell, I really don't think there will be any structural typing

[Anders Christiansen Sørby]

What do you think about adding lenses?

[Anders Christiansen Sørby]

I think adding lenses / optics would be even more powerful. If one could have some short hand syntax for indicating that a particular lens instance would be present s : { a : A } would mean {S : Type u} [Lens S A] (s : S)

[Sebastian Ullrich]

I don't think it's likely that this will end up in Lean itself, but of course extensibility is the whole point of Lean 4! We currently lack some kind of "binder macros" for doing something like that, but it's a topic that has come up before.

[Anders Christiansen Sørby]

I've done some preliminary work to add lenses in lean. Although I'm not sure type classes is the correct tool. Lenses have to be first class

def Lens (a b s t : Type u) : Type u := Para [] [] a b s t

def Lens' (s a : Type u) : Type u := Lens s s a a

I've based this on Agda which has a lot of good lens libraries.
This is particularly useful when doing more practical software engineering. Probably not so useful for pure math except perhaps category theory (but they would probably define their own syntax anyway)?