Update documentation and changelog for string interpolation (#2013)

* Update documentation and changelog for string interpolation

* Fix typo in changelog

* fix documentation about desugaring of interpolate

* Update CHANGELOG.md

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

CHANGELOG.md

@@ -10,6 +10,30 @@
 * New option `evaltiming` to time how long an evaluation takes at the REPL,
   set with `:set evaltiming`.
 
+### Language changes
+
+* Interpolated strings now make use of `concat` which is compiled into `fastConcat`
+  The interpolated slices now make use of the `Interpolation` interface available
+  in the prelude. It has only one method `interpolate` which is called for every
+  expression that appears within an interpolation slice.
+
+  ```idris
+  "hello \{world}"
+  ```
+
+  is desugared into
+
+  ```idris
+  concat [interpolate "hello ", interpolate world]
+  ```
+
+  This allows you to write expressions within slices without having to call `show`
+  but for this you need to implement the `Interpolation` interface for each type
+  that you intend to use within an interpolation slice. The reason for not reusing
+  `Show` is that `Interpolation` and `Show` have conflicting semantics, typically
+  this is the case for `String` which adds double quotes around the string.
+
+
 ## v0.5.0
 
 ### Language changes

docs/source/reference/strings.rst

@@ -133,5 +133,47 @@ string, since interpolated strings require the first ``{`` to be escaped, an int
 in a raw string uses ``\#{`` as starting delimiter.
 
 Additionally multiline strings can also be combined with string interpolation in the way you
-expect, as shown with ``Decl``. Finally all three features can be combined together in the
-last example, where a multiline string has a custom escape sequence and includes an interpolated slice.
+expect, as shown with the ``Decl`` pattern. Finally all three features can be combined together in the
+last branch of the example, where a multiline string has a custom escape sequence and includes an
+interpolated slice.
+
+Interpolation Interface
+-----------------------
+
+The Prelude exposes an ``Interpolation`` interface with one function ``interpolate``. This function
+is used within every interpolation slice to convert an arbitrary expression into a string that can
+be concatenated with the rest of the interpolated string.
+
+To go into more details, when you write ``"hello \{username}"`` the compiler translates the expression
+into ``concat [interpolate "hello ", interpolate username]`` so that the concatenation is fast and so that if
+``username`` implement the ``Interpolation`` interface, you don't have to convert it to a string manually.
+
+Here is an example where we reuse the ``Expr``
+type but instead of implementing a ``print`` function we implement ``Interpolation``:
+
+.. code-block::
+
+  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}
+          """
+          """#
+
+As you can see we avoid repeated calls to ``print`` since the slices are automatically applied to
+``interpolate``.
+
+We use ``Interpolation`` instead of ``Show`` for interpolation slices because the semantics of ``show``
+are not necessarily the same as ``interpolate``. Typically the implementation of ``show`` for ``String``
+adds double quotes around the text, but for ``interpolate`` what we want is to return the string as is.
+In the previous example, ``"hello \{username}"``, if we were to use ``show`` we would end up with the string
+``"hello "Susan`` which displays an extra pair of double quotes. That is why the implementation of
+``interpolate`` for ``String`` is the identity function: ``interpolate x = x``. This way the desugared
+code looks like: ``concat [id "hello ", interpolate username]``.