What is `opaque`?

Stream: lean4

[Hanting Zhang]

What does it mean that a constant is defined by opaque? I suspect it's not very deep, but also, I can't seem to find any documentation explaining what it actually is. :thinking:

[Henrik Böving]

To my knowledge an opaque keyword doesn't exist although the compiler does internally use this naming for constant declarations.

A constant declaration is one that cannot be unfolded (this is the opaque-ness) so it only requires a proof that its type is inhabited in order to keep the system consistent (otherwise it would be an axiom). constants are a rather rare sight but do have their use cases most commonly in partial defs which are desugared to something that includes a constant and when interacting with the FFI

[Hanting Zhang]

I see, that makes some sense. I'm now confused to what you mean by "constant," though, since there seems to be no reference of it in how Lean defined declarations.

/-- Declaration object that can be sent to the kernel. -/
inductive Declaration where
  | axiomDecl       (val : AxiomVal)
  | defnDecl        (val : DefinitionVal)
  | thmDecl         (val : TheoremVal)
  | opaqueDecl      (val : OpaqueVal)
  | quotDecl
  | mutualDefnDecl  (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` or `partial`
  | inductDecl      (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool)
  deriving Inhabited

Are constants == declarations? Or something more restricted? (Sorry I might be really misunderstanding you here)

[Henrik Böving]

As i said, the compiler interally calls constants opaque

[Henrik Böving]

so the representation here is the opaqueDecl

[Mac]

@Leonardo de Moura I remember we discussed renaming the constant keyword to opaque. If we still plan on doing that, it would probably be good to do it as soon as possible to minimize migration cost (and definitely before a first official release of Lean 4).

[Mac]

It would also remove the discrepancy discussed here.

[Hanting Zhang]

Henrik Böving said:

As i said, the compiler interally calls constants opaque

Ah ok, I understand now; constant isn't a thing in lean, it's just a human term, which the compiler calls opaque instead.

[Hanting Zhang]

Thanks!

[Mac]

Hanting Zhang said:

Ah ok, I understand now; constant isn't a thing in lean, it's just a human term, which the compiler calls opaque instead.

No, constant is a thing in Lean. It is a command that declares an opaqueDecl and has a similar syntax to def/axiom. For example:

constant Foo : Type
constant opaqueList : List Nat := [1,2,3]

[Mac]

There is also a different notion of a constant in the Lean core (e.g., ConstantInfo) that roughly corresponds to any defined symbol.

[Leonardo de Moura]

Mac said:

Leonardo de Moura I remember we discussed renaming the constant keyword to opaque. If we still plan on doing that, it would probably be good to do it as soon as possible to minimize migration cost (and definitely before a first official release of Lean 4).

I agree. It would be great to have a community consensus on this. @Sebastian Ullrich @Gabriel Ebner @Mario Carneiro @Wojciech Nawrocki @Edward Ayers Any thoughts/ideas?

[Hanting Zhang]

Mac said:

Hanting Zhang said:

Ah ok, I understand now; constant isn't a thing in lean, it's just a human term, which the compiler calls opaque instead.

No, constant is a thing in Lean. It is a command that declares an opaqueDecl and has a similar syntax to def/axiom. For example:

constant Foo : Type
constant opaqueList : List Nat := [1,2,3]

Oh! Ok this is indeed a confusing name discrepancy...

[Wojciech Nawrocki]

Using opaque instead of constant would make all commands match the internal definition kind list, and would clarify that it is not the same thing as Expr.const, so I would lean very slightly towards opaque, but this is not a strongly held view.

[Wojciech Nawrocki]

There is also the complication that constants are opaque from the kernel's point of view, but they evaluate just fine in the interpreter.