Multiline strings and string interpolation

[dhall-lang]

Multiline strings and string interpolation

[Gabriella439]

Newer versions of Dhall support multiline strings using the same syntax and semantics as Nix, like this:

{ example = ''
    This is a multi-line
    string that will have leading
    indentation stripped
  ''
}

However, Dhall doesn't support string interpolation yet, but I'm happy to add that

[markus1189]

I think @Gabriel439 didn't have a close look at what you are interpolating ;)

I don't think that we will ever allow interpolation of Haskell code. (Correct me Gabriel if I'm wrong)

What could be supported as string interpolation is to have dhall expressions like:

{ example = "${+1 + +2}" }

to get

{ example = "3" }

[Gabriella439]

Right, I understand that whether or not to provide a Natural → Text primitive is orthogonal to how to structure the Show interface for more complex types. I was just giving @markus1189 a heads-up for what issues he might run into when implementing Show for types like List

However, I don't think Natural/show : Natural → Text should drop the plus. If you want to render without the plus then there should be a separate Natural/toInteger : Natural → Integer and then an Integer/show : Integer → Text. In other words, your example would be:

λ(rating : { name : Text, rating : Natural }) → ''
# My thoughts about ${rating.name} (${Integer/show (Natural/toInteger rating.rating)} out of 5)

Also, I realized that there is no need to worry about rendering different bases (i.e. binary/hexademical/etc.) since the scope of a show-like function is to just to match the same input format as Dhall, which currently only supports decimal anyway. So I think it's fine to start by adding three new built-in functions:

• Natural/show : Natural → Text
• Integer/show : Integer → Text
• Natural/toInteger : Natural → Integer

That should probably solve @anfelor's use case and I'm pretty sure we will need those functions no matter what higher-level interface we provide in the Prelude

[anfelor]

Thank you, that would be great! Could you give a rough time line on when that feature will be available?

[anfelor]

@markus1189 You are right, I wrote the example in Haskell syntax, but I only want to express rendering a data type. I never worked with dhall before, so maybe I got this wrong, but shouldn't it be possible to write a function that takes a record and returns a string? Not show, more something in the form of:

let renderRating rating = ''
# My thoughts about ${rating.name} (${rating.rating} out of 5)
''

[markus1189]

That should be fine :)

…

On May 5, 2017 21:59, "Anton Felix Lorenzen" ***@***.***> wrote: @markus1189 <https://github.com/markus1189> You are right, I wrote the example in Haskell syntax, but I only want to express rendering a data type. I never worked with dhall before, so maybe I got this wrong, but shouldn't it be possible to write a function that takes a record and returns a string? Not show, more something in the form of: let renderRating rating = '' # My thoughts about ${rating.name} (${rating.rating} out of 5) '' — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#47 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAkGz8dMtTwFoDVajHOF-LXMbujLjj2rks5r23-tgaJpZM4NRtFU> .

[Gabriella439]

Yeah, @markus1189 is correct and I meant interpolating Text values into a string and not interpolating Haskell code, but it sounds like that is what you both meant anyway

My only caveat is that I might require the interpolated value to be Text and all other types would require an explicit conversion to Text for interpolation, such as:

{ example = "${Natural/toText (+1 + +2)}" }

That would imply that if you want to display a Natural then the language needs to provide an (efficient) Natural → Text primitive. The only reason I haven't provided such a primitive so far is that I wasn't sure whether or not Dhall should support multiple bases for string conversion (i.e. binary vs decimal vs hex)

I estimate this would conservatively take a few weeks for me to implement based on my upcoming schedule

[Gabriella439]

Also, as a side note, I've been considering releasing a small dhall-to-text utility for this purpose (i.e. using Dhall as a template language for rendering text), which just checks that the provided value has type Text and then outputs the normalized result as unqouted Text. If you would find that useful I can put up a small package for that

[anfelor]

No, I don't need such an utility as I use the Entry constructor fields for some features (page title and meta information, twitter cards, sidemaps, etc.).

[markus1189]

@Gabriel439 what do you think about opening an issue that collects the status of implementing string interpolation? If I can I might implement some of the X -> Text primitives, where X in { Natural, Integer, Bool, List, Double, ??? }, unless you already have ;)

We could even track the progress via a TODO list, s.t. anybody can jump in and give it a try

[Gabriella439]

@markus1189: Sure! However, there are two things worth noting:

First, there are a couple of primitives don't require primitive support. For example, you can do List and Bool without any primitive support. For example, showing Bool is easy:

λ(b : Bool) → if b then "True" else "False"

... and showing List is easy if you use trailing commas:

    λ(a : Type)
→   λ(showElement : a → Text)
→   λ(xs : List a)
→   let interior
        =   List/fold
            a
            xs
            Text
            (λ(y : a) → λ(ys : Text) → showElement y ++ ", " ++ ys)
            ""
in  "[" ++ interior ++ "]"

... and you can also do it without trailing commas with a little extra complexity:

    λ(a : Type)
→   λ(showElement : a → Text)
→   λ(xs : List a)
→   let interior
        =   List/fold
            a
            xs
            < Empty : {} | NonEmpty : Text >
            (   λ(y : a)
            →   λ(ys : < Empty : {} | NonEmpty : Text >)
            →   merge
                {   Empty
                    =   λ(_ : {})
                    →   < NonEmpty = showElement y | Empty : {} >
                ,   NonEmpty 
                    =   λ(z : Text)
                    →   < NonEmpty = showElement y ++ ", " ++ z | Empty : {} >
                }
                ys : < Empty : {} | NonEmpty : Text >
            )
            < Empty = {=} | NonEmpty : Text >
in  merge
    { Empty    = λ(_ : {}) → "[]"
    , NonEmpty = λ(z : Text) → "[" ++ z ++ "]"
    }
    interior : Text

... although they aren't too efficient. They take a few seconds to render 1000 elements on my laptop so it might still be worth providing primitives if we can't optimize that

Second, the above code is actually wrong because you can't display an empty List without displaying the element type, too. That implies that a Show "instance" for a type really needs two fields:

let Show : ∀(a : Type) → Type
    = λ(a : Type) → { show : a → Text, type : Text }
in  Show

So, for example a Show "instance" for Bool would be:

let showBool : ./Show Bool
    =   { show = λ(b : Bool) → if b then "True" else "False"
        , type : "Bool"
        }
in  showBool

However, it's actually even more complicated than that because you need to keep track of when to display parentheses. For example, if you do:

-- Assuming
-- ./showList : ∀(a : Type) → ./Show a → ./Show (List a)
-- ./showBool : ./Show Bool

./showList (List Bool) (./showList Bool ./showBool)

... then you want to make sure that the type gets rendered correctly as:

List (List Bool)

... and not:

List List Bool

... and implementing that correctly within Dhall is possible, but tricky

[anfelor]

@Gabriel439, I am glad to see that you are working on this. However, a show function where show . read == id is not my primary concern; take, for example, what I posted before:

let renderRating rating = ''
# My thoughts about ${rating.name} (${showNat rating.rating} out of 5)
''

Here, the rating can't drop below zero, so you could model rating.rating as a Nat. But then the renderRating function would return: (+5 out of 5) which looks ugly. I primarily need practical show functions, namely {Nat, Integer} -> Text and a string interpolation syntax.

So, unless it conflicts with your vision for dhall, I would suggest we implement @markus1189's proposal and have a TODO list, so I could implement the things that are the most relevant for me, if you don't mind.

[Gabriella439]

Also, thinking more about what @anfelor said, in most cases users will not want a utility to show lists in the exact same form as Dhall, or anything even remotely close. Typically they will want to template items using their own list format, like this for example:

    let concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Text/concat
in  let map    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
in  λ(items : List Text)
→   "List of items:\n"
++  concat (map Text Text (λ(x : Text) → "* " ++ x ++ "\n") items)

[anfelor]

@Gabriel439, yes, for example, I am currently thinking whether to write the html as a dhall template. In that case, I would implement something like your code above.

[Gabriella439]

Sorry it took a while, but I finally have an implementation ready here: #60

Let me know if that is what you had in mind