Undefine lambda

Stream: lean4

[Sky Wilshaw]

Is there a way to undefine the special function syntax for λ?

variable {λ : Type _} -- unexpected token 'λ'; expected '_' or identifier

[Mario Carneiro]

No, undefining tokens is not allowed. But let's do it anyway:

import Lean

open Lean Parser

def Lean.Parser.Trie.isEmpty {α} (t : Trie α) : Bool := t matches .Node none .leaf

partial def Lean.Parser.Trie.erase {α} (t : Trie α) (s : String) : Trie α :=
  let rec loop : Trie α → String.Pos → Option (Trie α)
    | ⟨val, m⟩, i =>
      match s.atEnd i with
      | true  => some (Trie.Node none m)
      | false => do
        let c := s.get i
        let i := s.next i
        let t ← m.find compare c
        let t ← loop t i
        let m := if t.isEmpty then m.erase compare c else m.insert compare c t
        some ⟨val, m⟩
  (loop t 0).getD t

elab "delete_token" tk:str : command => do
  let tk := tk.getString
  let env ← getEnv
  let s := parserExtension.ext.getState env
  if let top :: states := s.stateStack then
    modifyEnv fun env =>
      let top := { top with state.tokens := top.state.tokens.erase tk }
      parserExtension.ext.setState env { s with stateStack := top :: states }

delete_token "λ"

example : Nat → Nat := fun λ => λ
                        -- ^ expected token

[Sky Wilshaw]

Good to know, thanks!

[Mario Carneiro]

It doesn't work, though. The reason is that even though we have undefined lambda as a token, it is still not an identifier character as determined by this function:

def isLetterLike (c : Char) : Bool :=
  (0x3b1  ≤ c.val && c.val ≤ 0x3c9 && c.val ≠ 0x3bb) ||                  -- Lower greek, but lambda
  (0x391  ≤ c.val && c.val ≤ 0x3A9 && c.val ≠ 0x3A0 && c.val ≠ 0x3A3) || -- Upper greek, but Pi and Sigma
  (0x3ca  ≤ c.val && c.val ≤ 0x3fb) ||                                   -- Coptic letters
  (0x1f00 ≤ c.val && c.val ≤ 0x1ffe) ||                                  -- Polytonic Greek Extended Character Set
  (0x2100 ≤ c.val && c.val ≤ 0x214f) ||                                  -- Letter like block
  (0x1d49c ≤ c.val && c.val ≤ 0x1d59f)                                   -- Latin letters, Script, Double-struck, Fractur

So we get the same error that one would get with fun д => д: it's not a legal identifier character

[Mario Carneiro]

sadly this definition is not extensible, so we can't do anything about it

[Sky Wilshaw]

Ah, I see, U+03BB is explicitly banned.

[Mario Carneiro]

However, that's not the end of the story: even if it's a token we can still make it a macro that expands to an identifier:

import Lean

macro "λ" : term => pure (Lean.mkIdent `«λ»)

example : Nat → Nat := fun λ => λ

and it works! This is the same trick that used to be used to make this work. (It's a bit leaky but you should be able to use it most places an identifier is legal.)

[Sky Wilshaw]

Huh, that's really interesting.

[Mario Carneiro]

also, just in case you were not aware, even reserved words and non-identifier characters can be used in identifiers if you wrap them in the guillemets as in «λ»

[Sky Wilshaw]

I think I've seen that trick before in a couple of places like lakefiles and with weird filenames.

[Sky Wilshaw]

And protected exists/forall lemmas.

[Henrik Böving]

Mario Carneiro said:

No, undefining tokens is not allowed. But let's do it anyway:

import Lean

open Lean Parser

def Lean.Parser.Trie.isEmpty {α} (t : Trie α) : Bool := t matches .Node none .leaf

partial def Lean.Parser.Trie.erase {α} (t : Trie α) (s : String) : Trie α :=
  let rec loop : Trie α → String.Pos → Option (Trie α)
    | ⟨val, m⟩, i =>
      match s.atEnd i with
      | true  => some (Trie.Node none m)
      | false => do
        let c := s.get i
        let i := s.next i
        let t ← m.find compare c
        let t ← loop t i
        let m := if t.isEmpty then m.erase compare c else m.insert compare c t
        some ⟨val, m⟩
  (loop t 0).getD t

elab "delete_token" tk:str : command => do
  let tk := tk.getString
  let env ← getEnv
  let s := parserExtension.ext.getState env
  if let top :: states := s.stateStack then
    modifyEnv fun env =>
      let top := { top with state.tokens := top.state.tokens.erase tk }
      parserExtension.ext.setState env { s with stateStack := top :: states }

delete_token "λ"

example : Nat → Nat := fun λ => λ
                        -- ^ expected token

This is the most cursed meta program I've seen you produce so far :P

[Mario Carneiro]

You can see I've taken the lessons from #general > PSA about trusting Lean proofs to heart. Lean is the language where no means "well..."

[Eric Wieser]

Why did we decide to change all the λs to fun in mathlib if it's so hard to actually use λ as a name anyway?

[Eric Wieser]

I thought the argument was always "I want to use λ for a variable"

[Mario Carneiro]

It is, but lambda is defined in core

[Mario Carneiro]

and it wasn't designed to be optional

[Eric Wieser]

Was the thinking that step one was remove λ from mathlib, and step 2 is complain loudly at core until it becomes optional?

[Mario Carneiro]

I think so

[Mario Carneiro]

My understanding is that the reason λ is actually a non-identifier character rather than simply a token like other reserved words is so that people can write λa => a (compare with funny => ny which does not work)

[Eric Wieser]

That seems pretty reasonable, but totally at odds with the decision by mathlib to not use λ at all

[Mario Carneiro]

This whole part of the code is directly lifted from lean 3

[Mario Carneiro]

including the bizarre identifier list

[Mario Carneiro]

which also excludes Pi even though it's not a token anymore

[Sky Wilshaw]

For some context, the project I'm working on has some ordinal parameters that on paper are named λ, κ, μ, so I have to awkwardly capitalise λ in code.

[Sky Wilshaw]

I'd hoped that with fun this wouldn't be an issue in Lean 4.

[Sky Wilshaw]

Mario Carneiro said:

so that people can write λa => a

But on the other hand this seems quite useful!

[Jannis Limperg]

You can also write «λ», which would perhaps be less crazy.

[Sky Wilshaw]

λ currently shows up in over 200 places, I don't really want to litter my code with guillemets that much.

[Jannis Limperg]

Oh sorry, Mario already said so. :man_facepalming:

[Sky Wilshaw]

It doesn't really make sense to rename the ordinals either, because λ takes the role of a limit ordinal.

[Mario Carneiro]

how about ⲗ or Ⲗ?

[Sky Wilshaw]

Somewhat expectedly I get expected token using either of those.

[Mario Carneiro]

oh, they are coptic letters so I would have guessed they would fall under the identifier classification

[Sky Wilshaw]

They're U+2C9(6|7), which apparently aren't in the range.

[Sky Wilshaw]

image.png

[Sky Wilshaw]

Not to be confused with...
image.png

[James Gallicchio]

if mathlib can survive fine without lambda for functions, I think that's pretty good evidence that everyone will survive without lambdas for functions :p

[James Gallicchio]

(wrt the core change)