Idris 中的字符串字面量

为了方便字符串字面量的使用，Idris 除了普通字符串字面量外，还提供了三种特性：多行字符串（multiline strings）、原始字符串（raw strings）和插值字符串（interpolated strings）。

普通字符串字面量

字符串字面量的行为与其他编程语言类似。将你想作为字符串使用的文本用引号 " 包裹即可：

"hello world"

如重载字面量所述，字符串字面量可以重载为返回非 string 类型的值。

多行字符串字面量

有时你需要显示跨越多行的大段字符串字面量。此时可以使用 多行字符串字面量，它允许你将字符串分布在多行，保留换行和缩进。此外，你还可以根据周围代码缩进多行字符串，而不会破坏字符串的原始格式。

要使用多行字符串，先输入三引号 """ 并换行，然后输入你的文本，最后用左侧带有空白的三引号 """ 结束。结束三引号的缩进将决定每行文本应去除多少前导空白。

备注

多行字符串使用三引号，可以在多行块缩进时自动裁剪每行的前导空白。

welcome : String
welcome = """
    Welcome to Idris 2

    We hope you enjoy your stay
      This line will remain indented with 2 spaces
    This line has no intendation
    """

打印变量 welcome 会得到如下文本：

Welcome to Idris 2

We hope you enjoy your stay
  This line will remain indented with 2 spaces
This line has no intendation

可以看到，每行的前导 4 个空格都被去除了，这是因为结束定界符缩进了 4 个空格。

使用多行字符串字面量时，请注意以下几点：

起始定界符后必须紧跟换行
结束定界符的缩进级别不能超过任何一行的缩进

原始字符串字面量

在编写字符串字面量时，经常需要进行转义。对于普通字符串字面量，字符 \ 和 " 需要转义；对于多行字符串，字符 """ 需要转义。原始字符串字面量允许你动态更改所需的转义序列，从而避免频繁转义常见字符。为此，使用 #" 作为起始定界符，"# 作为结束定界符。可以增加 # 的数量，以适应 "# 也可能作为内容出现的特殊情况。如下例所示，使用原始字符串字面量后，匹配 \{ 时所需的 \\ 数量减半。

myRegex : Regex
myRegex = parseRegex #"\\{"#

如果你仍需转义字符，可以使用 \，后跟与定界符相同数量的 #。下例中我们用两个 # 作为转义序列，并希望打印一个换行符：

markdownExample : String
markdownExample = ##"markdown titles look like this: \##n"# Title \##n body""##

最后一个例子可以通过结合原始字符串字面量和多行字符串来实现：

markdownExample : String
markdownExample = ##"""
    markdown titles look like this:
    "# Title
    body"
    """##

插值字符串（Interpolated strings）

将字符串字面量与运行时值拼接是常见操作，但代码中充斥大量 " 和 ++ 符号会影响可读性，甚至引入难以察觉的 bug。插值字符串允许你在字符串字面量中内联求值为字符串的表达式，避免手动拼接。要使用插值字符串，使用 \{ 开始插值片段，在其中编写 Idris 表达式，并用 } 结束。

print : Expr -> String
print (Var name expr) = "let \{name} = \{print expr}"
print (Lam arg body) = #"\\#{arg} => \#{print body}"#
print (Decl fname fargs body) = """
    func \{fname}(\{commasep fargs}) {
        \{unlines (map print body)}
    }
    """
print (Multi lns) = #"""
    """
    \#{unlines lns}
    """
    """#

如第二行所示，原始字符串字面量和插值字符串可以结合使用。起始和结束定界符指示字符串中需要多少个 # 作为转义序列。由于插值字符串要求第一个 { 被转义，因此在原始字符串中的插值片段使用 \#{ 作为起始定界符。

此外，多行字符串也可以与字符串插值结合使用，如 Decl 模式所示。最后，三种特性可以在同一个例子中结合：多行字符串自定义转义序列，并包含插值片段。

插值接口（Interpolation Interface）

Prelude 提供了一个 Interpolation 接口，包含一个函数 interpolate。该函数用于每个插值片段，将任意表达式转换为可与插值字符串其他部分拼接的字符串。

更具体地说，当你写下 "hello \{username}" 时，编译器会将其转换为 concat [interpolate "hello ", interpolate username]，这样拼接更高效。如果 username 实现了 Interpolation 接口，你无需手动将其转换为字符串。

下面是一个例子，我们复用了 Expr 类型，但实现的不是 print 函数，而是 Interpolation：

Interpolation Expr where
    interpolate (Var name expr) = "let \{name} = \{expr}"
    interpolate (Lam arg body) = #"\\#{arg} => \#{body}"#
    interpolate (Decl fname fargs body) = """
        func \{fname}(\{commasep fargs}) {
            \{unlines (map interpolate body)}
        }
        """
    interpolate (Multi lns) = #"""
        """
        \#{unlines lns}
        """
        """#

可以看到，我们避免了多次调用 print，因为插值片段会自动应用 interpolate。

我们在插值片段中使用 Interpolation 而不是 Show，因为 show 的语义与 interpolate 不完全相同。通常，String 的 show 实现会在文本两侧加上双引号，而 interpolate 则直接返回原字符串。例如在前面的例子 "hello \{username}" 中，如果用 show，结果会变成 "hello "Susan，多了一对双引号。因此，String 的 interpolate 实现就是恒等函数：interpolate x = x。这样反糖后的代码就是 concat [id "hello ", interpolate username]。