Zulip Chat Archive

Stream: lean4

Topic: What is `opaque`?


Hanting Zhang (Jun 03 2022 at 17:39):

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 (Jun 03 2022 at 17:52):

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 (Jun 03 2022 at 18:01):

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 (Jun 03 2022 at 18:07):

As i said, the compiler interally calls constants opaque

Henrik Böving (Jun 03 2022 at 18:07):

so the representation here is the opaqueDecl

Mac (Jun 03 2022 at 18:09):

@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 (Jun 03 2022 at 18:10):

It would also remove the discrepancy discussed here.

Hanting Zhang (Jun 03 2022 at 18:13):

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 (Jun 03 2022 at 18:13):

Thanks!

Mac (Jun 03 2022 at 18:15):

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 (Jun 03 2022 at 18:16):

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 (Jun 03 2022 at 19:26):

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 (Jun 03 2022 at 19:28):

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 (Jun 03 2022 at 19:59):

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 (Jun 03 2022 at 20:01):

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


Last updated: Dec 20 2023 at 11:08 UTC