dhall-1.7.0: Prelude/Text/concatMapSep

{-
Transform each value in a `List` to `Text` and then concatenate them with a
separator in between each value

Examples:

```
./concatMapSep ", " Integer Integer/show [0, 1, 2] = "0, 1, 2"

./concatMapSep ", " Integer Integer/show ([] : List Integer) = ""
```
-}
    let concatMapSep
        : ∀(separator : Text) → ∀(a : Type) → (a → Text) → List a → Text
        =   λ(separator : Text)
          → λ(a : Type)
          → λ(f : a → Text)
          → λ(elements : List a)
          →     let status =
                      List/fold
                      a
                      elements
                      < Empty : {} | NonEmpty : Text >
                      (   λ(element : a)
                        → λ(status : < Empty : {} | NonEmpty : Text >)
                        → merge
                          { Empty    =
                              λ(_ : {}) → < NonEmpty = f element | Empty : {} >
                          , NonEmpty =
                                λ(result : Text)
                              → < NonEmpty = f element ++ separator ++ result
                                | Empty    : {}
                                >
                          }
                          status
                          : < Empty : {} | NonEmpty : Text >
                      )
                      < Empty = {=} | NonEmpty : Text >
            
            in  merge
                { Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result }
                status
                : Text

in  concatMapSep