Export smart constructor but also the type

Stream: lean4

[cognivore]

In X.lean:

private structure Name (x : String) where
  val : String := x
  deriving Repr

def isIdChar (x : Char) : Bool :=
  x.isAlphanum || "_.+-*/\\^~=<>!?@#$%&|:'`".data.elem x

def mkName (xs : String) : Option (Name xs) :=
  let xs' := xs.data
  if xs'.length == 0 then
    .none
  else
    if List.foldl (fun a x => if a then isIdChar x else false) true xs.data then
      .some {}
    else
      .none

in Main.lean:

import X
open X

def sameName (_n₁ : Name x) (_n₂ : Name x) : Name "Україна" := {}

This fails because Main can't refer to type Name. However, if I drop private, then I can construct an "invalid" type Name "Україна".

How would you approach this tradeoff?

[Leonardo de Moura]

You can use a private constructor.

structure Name (x : String) where
  private mk ::
  val : String := x
  deriving Repr

You may also tag val as private if you want.
BTW, I just pushed a fix for the { .. } since it was not checking whether the constructor was private or not.
It is also important to keep in mind that meta-programming can be used to access private names.

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/ef9127487ad9ed4ffc5dea4694f24a5a7fa820c4

[Gabriel Ebner]

So is the idea private fields/constructors should not be accessible unless you manually write a Expr.const `_private.. ..? There are so many ways around it that I always thought of private as more of a namespacing thing (like protected), and we certainly use it that way in core (to hide auxiliary definitions from the global namespace).

Around the private constructor:

• ⟨..⟩
• {..} (you've already fixed that one)
• by constructor

Around the private projections:

• let ⟨val⟩ := x; val
• by cases val; assumption

[Leonardo de Moura]

So is the idea private fields/constructors should not be accessible unless you manually write a Expr.const `_private.. ..?

Yes, the goal is to support scenarios like the one @cognivore described.

There are so many ways around it that I always thought of private as more of a namespacing thing (like protected), and we certainly use it that way in core (to hide auxiliary definitions from the global namespace).

I will fix them. I thought I had fixed {..} in the past, and I was surprised when it did not work this morning.

Around the private constructor: ⟨..⟩

This is one it is easy to fix.

by constructor

Not sure about this one. The scenarios I had in mind are for people using Lean as a programming language. If people start using the tactic framework for coding we may want to support this one too.

Similar for projections.

[Mario Carneiro]

Just to add on what Gabriel said: Although we can maybe patch some holes in being able to peer through private, I think you should not ever expect it to become as air tight as privacy in ML or Rust because the kernel / defeq can see through privacy. You should use opaque if you want to block this, but be aware that opaque is not scope-sensitive, so you have to wrap everything behind the privacy barrier in a structure which is then passed to opaque. See for example src4#FloatSpec.

For this particular pattern (using private to uphold invariants), there is a superior solution which is simply to put the invariants in the type:

namespace X

def isIdChar (x : Char) : Bool :=
  x.isAlphanum || "_.+-*/\\^~=<>!?@#$%&|:'`".data.elem x

structure Name (x : String) where
  private mk ::
  length_ne_zero : x.length ≠ 0
  all_isIdChar : x.data.all isIdChar
  deriving Repr

def mkName (xs : String) : Option (Name xs) :=
  let xs' := xs.data
  if h₁ : xs'.length = 0 then
    none
  else
    if h₂ : xs.data.all isIdChar then
      some { length_ne_zero := h₁, all_isIdChar := h₂ }
    else
      none

end X
open X

def sameName (_n₁ : Name x) (_n₂ : Name x) : Name "Україна" := {} -- fail

That way, even if the user manages to get past the privacy barrier using tricks, they still have to prove the same invariants that your smart constructor did. In fact, with this pattern it's probably not even necessary to hide the constructor - users are allowed to construct the thing directly as long as they prove the invariants, and the smart constructor is available if they don't want to.