Ordering strings

Stream: new members

[Christian Tzurcanu]

Mario Carneiro said:

the main user-level difference is that HashMap expects the keys to be hashable while RBMap expects the keys to be ordered

yes! That was one of my problems with RBMap: what function can I use for Ordering Strings?

it has tho have signature String -> String -> Ordering and I have tried String.compare and other things around: no luck. What do I have to import and what is this function (specifically to String and maybe to Int)?

[Eric Wieser]

You can use docs#Ord.compare

[Christian Tzurcanu]

Eric Wieser said:

You can use docs#Ord.compare

I have read around that and have already tried:

instOrdString

with the result:

application type mismatch
Lean.RBMap String ValueType instOrdString
argument
instOrdString
has type
Ord String : Type
but is expected to have type
String → String → Ordering : TypeL

now I tried: (Ord String) and it also errors

[Eric Wieser]

Did you try Ord.compare?

[Christian Tzurcanu]

Eric Wieser said:

Ord.compare

i should have

[Christian Tzurcanu]

pff it works. at least it seems

[Notification Bot]

6 messages were moved here from #maths > Defining a Type with multiple zeros by Eric Wieser.

[Eric Wieser]

(there's already enough discussion in that other thread, so I split this out)

[Notification Bot]

A message was moved from this topic to #new members > memory requirements by Eric Wieser.

[Christian Tzurcanu]

Christian Tzurcanu said:

Eric Wieser said:

Ord.compare

i should have

It seemed like it should work, but I don't understand how to set an empty RBMap:

def Dict := Lean.RBMap String ValueType Ord.compare

def dict : Dict := Lean.RBMap.empty String ValueType Ord.compare

errors: function expected at
Lean.RBMap.empty
term has type
Lean.RBMap ?m.576 ?m.577 ?m.578

so Ord.compare cannot be used in both circumstances?

[Eric Wieser]

The error message is telling you that you passed too many arguments

[Christian Tzurcanu]

Eric Wieser said:

The error message is telling you that you passed too many arguments

I have tried as much as I could to eliminate such trivial cases before posting my message. So I have tried with fewer arguments. And then I tried other things after your message. I'm such here.

[Eric Wieser]

Well, what happens if you use Lean.RBMap.empty String ValueType instead, removing the extra argument?

[Christian Tzurcanu]

Eric Wieser said:

Well, what happens if you use Lean.RBMap.empty String ValueType instead, removing the extra argument?

nothing of note. at least not obvious to me: i get this error: function expected at
Lean.RBMap.empty
term has type
Lean.RBMap ?m.582 ?m.583 ?m.584Lea

[Christian Tzurcanu]

is the difference between those numbers after ?m relevant?

[Damiano Testa]

Maybe just stopping at empty?

[Eric Wieser]

If you see "function expected" this pretty much always means either "you're still passing too many arguments", or "you made a typo and wrote x y instead of x + y, or f g x instead of f (g x)

[Christian Tzurcanu]

Damiano Testa said:

Maybe just stopping at empty?

that yields: function expected at
Lean.RBMap.empty
term has type
Lean.RBMap ?m.582 ?m.583 ?m.584Lean 4

Lean.RBMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Lean.RBMap α β cmp

[Christian Tzurcanu]

def dict Dict := Lean.RBMap.empty means stopping at empty

[Eric Wieser]

Could you make a #mwe?

[Eric Wieser]

What is ValueType?

[Christian Tzurcanu]

inductive ValueType
  | intValue (v : Int)
  | stringValue (v : String)
  | boolValue (v : Bool)

[Christian Tzurcanu]

but i see even if i use String instead of ValueType: its the same thing

[Christian Tzurcanu]

so that would be mve:

def Dict := Lean.RBMap String String Ord.compare
def dict Dict := Lean.RBMap.empty

[Kevin Buzzard]

Lean.RBMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Lean.RBMap α β cmp means "Lean.RBMap.empty takes no explicit arguments, all arguments are to be inferred by unification"; that's the meaning of the {} brackets. So Lean.RBMap.empty X will give you the error about how Lean expected a function, for any X.

[Christian Tzurcanu]

Kevin Buzzard said:

Lean.RBMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Lean.RBMap α β cmp means "Lean.RBMap.empty takes no explicit arguments, all arguments are to be inferred by unification"; that's the meaning of the {} brackets. So Lean.RBMap.empty X will give you the error about how Lean expected a function, for any X.

I have read your words. I did not understand yet.

[Damiano Testa]

This works:

import Lean

variable (ValueType)

def Dict := Lean.RBMap String ValueType Ord.compare

def dict : Dict ValueType := Lean.RBMap.empty

[Christian Tzurcanu]

so what is the the documentation for this: variable (a)

[Damiano Testa]

Hovering over variable, you should see the docs.

[Damiano Testa]

In this case, it is introducing a term of a generic type. It is also making it an explicit argument of wherever it is used.

[Damiano Testa]

With your code, Lean could not know just seeing dict : Dict what it should use for the "second" argument to Lean.RBMap. So, I made it explicit and passed it to Dict.

[Christian Tzurcanu]

Damiano Testa said:

With your code, Lean could not know just seeing dict : Dict what it should use for the "second" argument to Lean.RBMap. So, I made it explicit and passed it to Dict.

it's going to be magic for a while for me

[Christian Tzurcanu]

thank you. i have other problems now in the code with the introduction of that variable(). trying to make it work

[Damiano Testa]

Maybe if I had written the (arguably better)

universe u
variable (ValueType : Type u)

it would have been clearer.

[Eric Wieser]

Christian Tzurcanu said:

so that would be mve:

def Dict := Lean.RBMap String String Ord.compare
def dict Dict := Lean.RBMap.empty

This has a typo (and a missing import). It works fine without the typo:

import Lean

def Dict := Lean.RBMap String String Ord.compare
def dict : Dict := Lean.RBMap.empty

[Damiano Testa]

Ah, if you use String as the "second" type as well, then there is no ambiguity: this is why Lean does not need more info in this case.

[Eric Wieser]

Using the inductive ValueType above also make it work fine

[Eric Wieser]

This is why it's really important to provide a mwe, so that people can actually reproduce the problem you're having, and not an unrelated one that makes them give answers that confuse you more

[Christian Tzurcanu]

Eric Wieser said:

This is why it's really important to provide a mwe, so that people can actually reproduce the problem you're having, and not an unrelated one

thank you. i imagined i could do it with economy. and it is not possible. i need to do MWE. got it

[Damiano Testa]

Another advantage of trying to minimize your own problems is that frequently you solve them yourselves, which is, in the long run, faster than even asking the question!

[Christian Tzurcanu]

Eric Wieser said:

Using the inductive ValueType above also make it work fine

how can inductive ValueType work fine?

[Damiano Testa]

I consider that inductive ValueType "works" a bit of a joke...

[Damiano Testa]

In the sense that it literally does work, but it clearly is not what is intended! :smile:

[Damiano Testa]

inductive ValueType introduces a new type, that contains nothing at all. Exercise: can you name another type that is identical to inductive ValueType, except for its name? :upside_down:

[Christian Tzurcanu]

because now i have a problem presumably introduced by variable(ValueType)

import Lean.Data.RBMap
-- import Lean.Data.String
-- open Std

-- Define a type to encapsulate different types of values
inductive ValueType
  | intValue (v : Int)
  | stringValue (v : String)
  | boolValue (v : Bool)
  -- Add more types as needed

variable (ValueType)

-- Define a type alias for the RBMap with String keys and ValueType values
def Dict := Lean.RBMap String ValueType Ord.compare

-- Function to add an entry to the dictionary
def addEntry (dict : Dict) (key : String) (value : ValueType) : Dict :=
  dict.insert key value

The Dict does not seem to get defined: type expected, got
(Dict : Type ?u.519 → Type ?u.519)Lean 4

Dict.{u_1} (ValueType : Type u_1) : Type u_1

[Damiano Testa]

You should use variable x, if you intend to make your functions be valid for various different kinds of x.

[Christian Tzurcanu]

now i understand: https://live.lean-lang.org/ is very useful for these dialogues!

[Damiano Testa]

In your case, you seem to want to use the custom-made type that you called ValueType, so you should not make a completely arbitrary term that happens to be called also ValueType an available variable!

[Christian Tzurcanu]

Damiano Testa said:

In your case, you seem to want to use the custom-made type that you called ValueType, so you should not make a completely arbitrary term that happens to be called also ValueType an available variable!

yes, obviously

[Damiano Testa]

Ok, so... are you all good?

[Christian Tzurcanu]

Damiano Testa said:

Ok, so... are you all good?

no. i seem to be back at step1:

def dict : Dict := Lean.RBMap.empty would error

[Damiano Testa]

import Lean.Data.RBMap
-- import Lean.Data.String
-- open Std

-- Define a type to encapsulate different types of values
inductive ValueType
  | intValue (v : Int)
  | stringValue (v : String)
  | boolValue (v : Bool)
  -- Add more types as needed

-- let me remove this!
--variable (ValueType)

-- Define a type alias for the RBMap with String keys and ValueType values
def Dict := Lean.RBMap String ValueType Ord.compare

-- all good
def dict : Dict := Lean.RBMap.empty

[Eric Wieser]

Which is just combining the code you posted above, with the correction you said you'd already tried

[Damiano Testa]

You want to make sure that Lean uses your "inductively defined" ValueType. If you want to have a variable floating around, give it a different name, so that neither you nor Lean can get confused by it.

[Eric Wieser]

(I think this is a case of Damiano guessing what your question was because you didn't write it unambiguously, and then confusing you because his guess was not the one you were actually asking)

[Christian Tzurcanu]

Damiano Testa said:

import Lean.Data.RBMap
-- import Lean.Data.String
-- open Std

-- Define a type to encapsulate different types of values
inductive ValueType
  | intValue (v : Int)
  | stringValue (v : String)
  | boolValue (v : Bool)
  -- Add more types as needed

-- let me remove this!
--variable (ValueType)

-- Define a type alias for the RBMap with String keys and ValueType values
def Dict := Lean.RBMap String ValueType Ord.compare

-- all good
def dict : Dict := Lean.RBMap.empty

I have looked at every letter in your code: it is identical to my code. mine errors

[Damiano Testa]

There are commented out things in this code.

[Eric Wieser]

You could paste yours and that code into https://www.diffchecker.com/, and see the difference

[Eric Wieser]

Or "Compare new untitled text files" in vscode

[Christian Tzurcanu]

now it does not error, but i did not change the code. i restarted the file

[Christian Tzurcanu]

-- import Lean
import Lean.Data.RBMap
-- import Lean.Data.String
-- open Std

-- Define a type to encapsulate different types of values
inductive ValueType
  | intValue (v : Int)
  | stringValue (v : String)
  | boolValue (v : Bool)
  -- Add more types as needed

-- variable (ValueType)

-- Define a type alias for the RBMap with String keys and ValueType values
def Dict := Lean.RBMap String ValueType Ord.compare

-- Function to add an entry to the dictionary
def addEntry (dict : Dict) (key : String) (value : ValueType) : Dict :=
  dict.insert key value

-- Function to get an entry from the dictionary
def getEntry (dict : Dict) (key : String) : Option ValueType :=
  dict.find? key


def dict : Dict := Lean.RBMap.empty

def dict2 : Dict := addEntry dict "key1" (ValueType.intValue 42)

now it errors at the last line. so it does something unexpected

[Christian Tzurcanu]

Damiano Testa said:

There are commented out things in this code.

I commented out in my code too, at that time

[Eric Wieser]

now it errors at the last line. so it does something unexpected

Works in the web editor for me

[Eric Wieser]

Is there something at the end of the file you're not showing us? That can break stuff higher up

[Christian Tzurcanu]

Eric Wieser said:

now it errors at the last line. so it does something unexpected

Works in the web editor for me

error is: function expected at
addEntry dict "key1" (ValueType.intValue 42)
term has type
DictLean 4

addEntry (dict : Dict) (key : String) (value : ValueType) : Dict

[Eric Wieser]

Yeah, my bet is you have something at the bottom of the file you're not showing us

[Christian Tzurcanu]

getEntry dict2 "key1"

[Christian Tzurcanu]

Eric Wieser said:

Yeah, my bet is you have something at the bottom of the file you're not showing us

you were totally right

[Eric Wieser]

You probably wanted #eval before that line

[Eric Wieser]

Maybe we should update #mwe to point out this last-line gotcha

[Christian Tzurcanu]

yes. with eval: expression
getEntry dict2 "key1"
has type
Option ValueType
but instance
Lean.Eval (Option ValueType)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the Repr class also implements the Lean.Eval classLean 4

[Christian Tzurcanu]

-- import Lean
import Lean.Data.RBMap
-- import Lean.Data.String
-- open Std

-- Define a type to encapsulate different types of values
inductive ValueType
  | intValue (v : Int)
  | stringValue (v : String)
  | boolValue (v : Bool)
  -- Add more types as needed

-- variable (ValueType)

-- Define a type alias for the RBMap with String keys and ValueType values
def Dict := Lean.RBMap String ValueType Ord.compare

-- Function to add an entry to the dictionary
def addEntry (dict : Dict) (key : String) (value : ValueType) : Dict :=
  dict.insert key value

-- Function to get an entry from the dictionary
def getEntry (dict : Dict) (key : String) : Option ValueType :=
  dict.find? key


def dict : Dict := Lean.RBMap.empty

def dict2 : Dict := addEntry dict "key1" (ValueType.intValue 42)
-- def dict3 := addEntry dict2 "key2" (ValueType.stringValue "hello")
-- def dict4 := addEntry dict3 "key3" (ValueType.boolValue true)

#eval getEntry dict2 "key1"

[Eric Wieser]

That message isn't surprising, and contains some good hints

[Eric Wieser]

Think about what Lean needs to know to show you a Option ValueType

[Eric Wieser]

It probably knows how to print Option because that's built in; but it's never seen your ValueType before. And it mentions something about Repr...

[Christian Tzurcanu]

Eric Wieser said:

Think about what Lean needs to know to show you a Option ValueType

yes. i commented out the toString because other problems

[Eric Wieser]

ToString and Repr are slightly different things

[Christian Tzurcanu]

I think i should consider this solved and look on my own

[Christian Tzurcanu]

but.. i was surprized with things that error well ahead of their sequence.. in other places

[Christian Tzurcanu]

Eric Wieser said:

ToString and Repr are slightly different things

what is the custom? should I mark this as solved? (it was)

[Notification Bot]

Christian Tzurcanu has marked this topic as resolved.

[Kevin Buzzard]

(The custom is to not mark anything as resolved)

[Notification Bot]

Christian Tzurcanu has marked this topic as unresolved.