Does Lean Have a Symbol Primitive?

Stream: lean4

[James B Clifford]

I am new to lean. I was just wondering if lean had something similar to JavaScript's Symbol Primitive? Something guaranteed to be unique. https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/Symbol

[Mac]

Lean does not have a symbol primitive per say. However, the constructors of a inductive can function like them in many cases . For example, if there are three symbols I wish to use (foo, bar, and baz), I can create the following inductive to represent the symbol type:

inductive Symbol
| foo | bar | baz

However, this does requiring knowing all the symbols you plan on using ahead-of-time. Sadly, there is no way to lazily create guaranteed unique symbols in Lean (at least not without adding new axioms and if then it would be noncomputable).

[James B Clifford]

thank you for your reply. I was hoping to be able to create something that would scale out to infinity. I suppose an ever-incrementing counter would work in most cases.... does lean have the concept of a singleton class? (again, I'm sorry, this is all new to me)

[Jireh Loreaux]

If you wanted infinitely many distinct symbols, you can do that too:

inductive Symbol
  | foo : ℕ → Symbol

Then foo 1 and foo 2 or foo n for n : ℕ are distinct symbols. Is this what you were looking for? (Note: I'm not familiar with javascript, so this may be way off the mark.)

[Jason Rute]

If I understand correctly correctly, Jireh’s answer is one way to make a “singleton class”. Another is to use a structure with one field. Logically these are the same thing, but the latter has more bells and whistles.

[Jason Rute]

structure Symbol where
  n : Nat

[Arien Malec]

Generally inductive is a better fit for how one uses symbol in other languages (JS, Ruby) (where they are implemented as interned immutable strings).

[Arien Malec]

The benefit in a more expressive type system is that they can contain associated data, as @Jireh Loreaux notes.

[Kyle Miller]

For Jireh's/Jason's Symbol type, in practice you'd define a state monad with a constructor for creating fresh symbols while incrementing the state monad's internal counter.

Here's an example:

structure Symbol where
  n : Nat
deriving Repr

abbrev SymbolM := StateM Nat

def freshSymbol : SymbolM Symbol :=
  StateT.modifyGet (λ n => (Symbol.mk n, n + 1))

/-- Run a `SymbolM` computation, with the internal fresh symbol counter starting at `start`. -/
def SymbolM.run {α : Sort _} (m : SymbolM α) (start : Nat := 0) : α :=
  StateT.run' m start

-- Example: create an array of `num` fresh symbols
def freshSymbols (num : Nat) : SymbolM (Array Symbol) := do
  let mut symbols := #[]
  for _ in [0:num] do
    symbols := symbols.push (← freshSymbol)
  return symbols

#eval SymbolM.run (freshSymbols 10)
-- #[{ n := 0 }, { n := 1 }, { n := 2 }, { n := 3 }, { n := 4 }, { n := 5 }, { n := 6 }, { n := 7 }, { n := 8 }, { n := 9 }]

[Kyle Miller]

Since this is a functional programming language, you need to do the work yourself to keep track of the state. In this case, it's the necessary state to be able to tell different Symbols created at different times apart.

[Mac]

@Kyle Miller If James is just looking for how to make unique ids at the user level then your solution is the way to go.

However, generally, the goal of a symbol primitive in a language like JS is specifically to avoid carrying said generator state around at user level, Instead, the goal is have the language automatically ensure the different symbol literals used across the language are distinct. (essentially at a metaprogramming level).

[Mac]

For example, one might an expandable symbol type in Lean 4 to work something like this:

open_type Symbol
instance foo : Symbol
instance bar : Symbol
-- use foo and bar in code and later on (perhaps in a dependant package):
instance baz : Symbol

[Eric Wieser]

Presumably you could build a workable version of this by just making Symbol store a filename, line number, and column offset, and creating suitable notation that populates those arguments

[Kyle Miller]

@Mac Javascript doesn't have symbol literals, just the symbol constructor (it's not like Ruby or Lisp in this way). As far as I've known, the main intent for them is to provide unique non-string keys for private attributes in objects (keys can only be strings or symbols in JavaScript). There are also some special methods that objects can have at some specific symbols. Symbols can be used in the Lispier way if you create global constants for them first.

[Mac]

@Kyle Miller True. I was using the term literal a bit too loosely. The docs have a form of Symbol "literals" with @@symbol syntax but that is not reflecting the language itself (where @@foo is usually exposed as Symbol.foo).