String

String は文字列を表す型です。次のように、文字を表す型 Char のリストとして定義されています。

/-- 文字列 -/
structure String where
  /-- 文字列をほどいて `List Char` にする -/
  data : List Char

文字列結合

String.append を使って文字列を結合することができます。この関数は ++ という記号が割り当てられています。

#guard String.append "Hello, " "world!" = "Hello, world!"
#guard "Hello, " ++ "world!" = "Hello, world!"

文字列の長さ

文字列の長さは String.length 関数で取得することができます。

#guard "Hello".length = 5

#check List.length

String.length を素朴に実装すると、

  1. 文字列を List Char に変換する
  2. List.length を使って長さを求める

という手順になるかと思います。n 個の要素を持つ xs : List α に対して長さを求めようとすると、先頭から順に要素をたぐっていくので n に比例する時間がかかります。したがって String.length は長い文字列に対しては遅くなりそうなものですが、コンパイラによって実装がオーバーライドされているため、実際には n が大きくても高速に実行できます。

このあたりの背景は、次に示すようにドキュメントコメントに書かれています。

A string is a sequence of Unicode code points.

At runtime, strings are represented by dynamic arrays of bytes using the UTF-8 encoding. Both the size in bytes (String.utf8ByteSize) and in characters (String.length) are cached and take constant time. Many operations on strings perform in-place modifications when the reference to the string is unique.

文字列補間

String 型の変数の「評価した後の値」を文字列に埋め込むことができます。これを 文字列補間(string interpolation) と呼びます。Lean では、これは s! という構文で行うことができます。

def greet := "Hello"

/- info: "Hello, world!" -/
#eval s!"{greet}, world!"