Zulip Chat Archive

Stream: lean4

Topic: Should String.reverse be added?

Joseph O (May 27 2022 at 13:26):

Should a String.reverse be added to the std? I have found myself needing it quite a few times, and I even have an implementation in my Soup project:

def String.reverse := (String.intercalate "") ∘ (List.map toString) ∘ List.reverse ∘ String.toList

I also looked through the docs carefully and wasn't able to find one.

Arthur Paulino (May 27 2022 at 13:29):

You can make use of List.reverse:

def String.reverse (s : String) : String :=
  ⟨s.data.reverse⟩

Joseph O (May 27 2022 at 13:32):

Doesnt that return a list?
Or do the brackets do something special

Henrik Böving (May 27 2022 at 13:33):

The brackets are the anonymous constructor notation which you can use if the expected data type has only one constructor because what you want can be inferred perfectly then.

Joseph O (May 27 2022 at 13:33):

So it implicitly converts the list to a String?

Henrik Böving (May 27 2022 at 13:34):

No its quite explicit, after all you wrote it out

Joseph O (May 27 2022 at 13:35):

But I didn't call String.intercalate ""

Henrik Böving (May 27 2022 at 13:35):

That being said operating directly on Strings data field is mayube not what you really want to do? Strings have an FFI representation as evident by their constructors etc. being external functions https://github.com/leanprover/lean4/blob/d13fac6f458bd1efd772424066f2a85f8c8ba32a/src/Init/Prelude.lean#L1122-L1123 so you probably want to define this function either in terms of existing string functions or via the FFI

Joseph O (May 27 2022 at 13:36):

So you can construct a string with a list essentially? I guess it makes sense, as a string is a list of chars

Henrik Böving (May 27 2022 at 13:36):

Joseph O said:

But I didn't call String.intercalate ""

That doesnt matter at all, string is a structure around a list of characters so calling the constructor of that structure is the only thing you need to do, however as explained this "list of characters" is just the representation that is given to the lean programmer and not the one you usually want to work with

Joseph O (May 27 2022 at 13:37):

#eval (⟨['h', 'i']⟩ : String) -- "hi"

Joseph O (May 27 2022 at 13:37):

Henrik Böving said:

Joseph O said:

But I didn't call String.intercalate ""

That doesnt matter at all, string is a structure around a list of characters so calling the constructor of that structure is the only thing you need to do, however as explained this "list of characters" is just the representation that is given to the lean programmer and not the one you usually want to work with

Yeah I see
Thats pretty cool

Joseph O (May 27 2022 at 13:37):

But now to the original question, should this be added to the std

Arthur Paulino (May 27 2022 at 13:38):

Maybe in a future. I wouldn't worry about Std at the moment. The core devs have bigger fish to fry

Henrik Böving (May 27 2022 at 13:39):

As you've been told before, Std is the things the compiler needs to work and not a general purpose Std library that is receiving contributions right now so no, not unless the compiler needs it.

Joseph O (May 27 2022 at 13:46):

What about the case with HashMap.toList?

Joseph O (May 27 2022 at 13:46):

But if it isn't needed in the std, Ill probably add it in mathlib 4

Kyle Miller (May 27 2022 at 13:48):

String reversal is a questionable operation if there's not a specification for what it's supposed to do.

def String.reverse := (String.intercalate "") ∘ (List.map toString) ∘ List.reverse ∘ String.toList

#eval "mañana".reverse
-- "anãnam"

Joseph O (May 27 2022 at 13:49):

Well all it does it reverse a string

Kyle Miller (May 27 2022 at 13:50):

I might have expected anañam if you just told me that this reverses strings.

Kyle Miller (May 27 2022 at 13:51):

There's also grapheme cluster reversal. Codepoint reversal is valid, but my point is that there's not just one string reversal operation.

Joseph O (May 27 2022 at 13:51):

Ah right

Last updated: Dec 20 2023 at 11:08 UTC