Custom constructors for structures

Stream: general

[Oleks]

Declaring a structure σ declares a σ.mk operation. Can I suppress this, and instead declare a custom constructor for σ's?

[Kevin Buzzard]

The default constructor needs to exist but you can name it what you like with the name :: syntax. See for example the beautiful definition of ULift:

structure ULift.{r, s} (α : Type s) : Type (max s r) where
  /-- Lift a value into `ULift α` -/    up ::
  /-- Extract a value from `ULift α` -/ down : α

so now we have ULift.up and ULift.down doing what you'd expect them to do (and no ULift.mk).

[Oleks]

I don't quite understand :: and : α above.

[Oleks]

Maybe I'm just unfamiliar with declaring structures with the where keyword.

[Oleks]

Perhaps more to the point, how can I have a custom body for up in this example?

[Henrik Böving]

You can't, a constructor is a very primitive part of both the type theory and the runtime. In type theory it has special properties such as being able to use it for induction/case splitting, in the runtime the constructor precisely describes the kind of struct you need to allocate to store a type. If you want to have custom additional stuff in a constructor you can write something like:

structure Foo where
  private internalMk ::
    bar : Nat

def Foo.mk (bar : Nat) : Foo :=
  let customStuff = bar * 2
  Foo.internalMk bar

The term constructor is not equivalent to the one from classical OOP languages.

[Matthew Ballard]

Out of curiosity, what would you generally call Foo.mk to distinguish it from Foo.internalMk here?

[Henrik Böving]

There is no need for that, internalMk is private so an outside user doesn't see it. Though of course if you want to prove things about Foo this get's more involved, then again, if you prove stuff about Foo you probably don't want custom stuff in a constructor anyway

[Matthew Ballard]

Let me try again. Are both constructors?

[Henrik Böving]

Not in the Lean sense no

[Matthew Ballard]

What would you call Foo.mk then

[Henrik Böving]

I don't have a name for it, some versions of Foo.mk (though not this one) might be labeled smart constructors in other FP languages

[Matthew Ballard]

Here is what I used #20993 when I asked myself this question. A problem is that many (most?) people will just call them all "constructors"

[Matthew Ballard]

I am mainly looking for better alternatives

[Henrik Böving]

You can call them constructors if you want, it makes sense from an OOP perspective. But people that do type theory or work with meta code will be confused.

[Oleks]

The reason I ask is precisely because I want to prove things about my structure. As an example, let's say I want to implement a NonEmptyArray based on the underlying Array type. Then I would like to limit how NonEmptyArray may be constructed, so that no-one can construct a NonEmptyArray with an empty array underneath. If I can limit how NonEmptyArray may be constructed, I can leverage the fact that it is non-empty in subsequent proofs.

[Kyle Miller]

In that case, you can add an additional proposition field that the underlying array is nonempty. That enforces the constraint that you want.

[Kyle Miller]

structure NonEmptyArray (α : Type _) where
  toArray : Array α
  nonempty : ¬ toArray.isEmpty

[Kyle Miller]

Here's an example of conditionally constructing one at runtime:

def NonEmptyArray.mk? {α} (array : Array α) : Option (NonEmptyArray α) :=
  if h : ¬ array.isEmpty then
    some { toArray := array, nonempty := h }
  else
    none