[ prelude ] Give every Show type a default Interpolation

[andylokandy]

Now every type implemented Show is allowed to be interpolated into strings without following a show.

Previous discussion on #1967 (comment)

[andylokandy]

cc @mattpolzin @gallais @andrevidela

[andylokandy]

Thanks to @ohad for the suggestion, we're now resolving the ambiguity explicitly by runtime pattern matching on the type a. In most cases, the type a should be able to be erased during the compilation.

[gallais]

I'm not sure I'm comfortable merging this without good evidence it does not imply hanging onto
more types at runtime.

[andylokandy]

I tried to codegen two samples into chez scheme, it seems that the type indeed get earased, but because I'm not familiar with scheme I'm not 100% sure about it.

-- with runtime `a : Type`

main : IO ()
main = putStr (interpolate True)

(define Main-main(blodwen-lazy (lambda () (PreludeC-45IO-putStr (cons (vector (vector (lambda (u--b) (lambda (u--a) (lambda (u--func) (lambda (arg-8478) (lambda (eta-0) (PreludeC-45IO-u--map_Functor_IO u--func arg-8478 eta-0)))))) (lambda (u--a) (lambda (arg-9181) (lambda (eta-0) arg-9181))) (lambda (u--b) (lambda (u--a) (lambda (arg-9187) (lambda (arg-9194) (lambda (eta-0) (let ((act-17 (arg-9187 eta-0))) (let ((act-16 (arg-9194 eta-0))) (act-17 act-16))))))))) (lambda (u--b) (lambda (u--a) (lambda (arg-9661) (lambda (arg-9664) (lambda (eta-0) (let ((act-24 (arg-9661 eta-0))) ((arg-9664 act-24) eta-0))))))) (lambda (u--a) (lambda (arg-9675) (lambda (eta-0) (let ((act-51 (arg-9675 eta-0))) (act-51 eta-0)))))) (lambda (u--a) (lambda (arg-10912) arg-10912))) (PreludeC-45Interpolation-u--interpolate_Interpolation_interpShowC-36a (cons (lambda (u--x) (PreludeC-45Show-u--show_Show_Bool u--x)) (lambda (u--d) (lambda (u--x) (PreludeC-45Show-u--showPrec_Show_Bool u--d u--x)))) 1)))))

(define PreludeC-45Interpolation-u--interpolate_Interpolation_interpShowC-36a (lambda (arg-1 arg-2) (let ((e-1 (car arg-1))) (e-1 arg-2))))

---

-- w/o runtime `a : Type`

module Main

%hide interpDefault

Interpolation Bool where
  interpolate = show

main : IO ()
main = putStr (interpolate True)

(define Main-main(blodwen-lazy (lambda () (PreludeC-45IO-putStr (cons (vector (vector (lambda (u--b) (lambda (u--a) (lambda (u--func) (lambda (arg-8478) (lambda (eta-0) (PreludeC-45IO-u--map_Functor_IO u--func arg-8478 eta-0)))))) (lambda (u--a) (lambda (arg-9181) (lambda (eta-0) arg-9181))) (lambda (u--b) (lambda (u--a) (lambda (arg-9187) (lambda (arg-9194) (lambda (eta-0) (let ((act-17 (arg-9187 eta-0))) (let ((act-16 (arg-9194 eta-0))) (act-17 act-16))))))))) (lambda (u--b) (lambda (u--a) (lambda (arg-9661) (lambda (arg-9664) (lambda (eta-0) (let ((act-24 (arg-9661 eta-0))) ((arg-9664 act-24) eta-0))))))) (lambda (u--a) (lambda (arg-9675) (lambda (eta-0) (let ((act-51 (arg-9675 eta-0))) (act-51 eta-0)))))) (lambda (u--a) (lambda (arg-10912) arg-10912))) (Main-u--interpolate_Interpolation_Bool 1)))))

(define Main-u--interpolate_Interpolation_Bool (lambda (ext-0) (PreludeC-45Show-u--show_Show_Bool ext-0)))

[stefan-hoeck]

Sorry for chiming in here, but I'm not sure that this is really an improvement over the status quo. I think there was an agreement that Show and Interpolation have different semantics, but with this PR we make it harder for programmers to write and use custom implementations instead of using the default, which is based on Show. If I understand correctly, custom implementations will require a %hide interpDefault to work correctly if they also come with a Show implementation, in which case all data types using interpDefault will no longer be available during interpolation. I wonder if it's such a bad thing to require a single line of code for every implementation of Interpolation:

Interpolation Foo where interpolate = show

[andylokandy]

@stefan-hoeck In 99.99% of the cases, you won't add your own Interpolation implementation, you will explicitly convert it into String, e.g. to print an integer in hexadecimal while another one in binary: "\{hex 100} \{bin 100}". The most significant reason for having Interpolation instead of Show is to specially handle String.

custom implementations will require a %hide interpDefault to work correctly if they also come with a Show implementation, in which case all data types using interpDefault will no longer be available during interpolation

According to @ohad's comment, the custom implementations on type coming with Show implementation is inherit ambiguous. It's also not difficult to resolve it: define your own interpDefault which includes your custom type as an exception just like String.

[stefan-hoeck]

@stefan-hoeck In 99.99% of the cases, you won't add your own Interpolation implementation, you will explicitly convert it into String, e.g. to print an integer in hexadecimal while another one in binary: "\{hex 100} \{bin 100}". The most significant reason for having Interpolation instead of Show is to specially handle String.

If this is true, why do we even need the Show a => Interpolation a default case at all? My fear is that this adds a significant layer of complexity and obscurity to the Prelude, which is - according to your numbers - hardly ever needed. Why can't we just have

Interpolation String where interpolate x = x

and nothing else in the Prelude?

[andylokandy]

I mean Interpolation String + Show a => Interpolation a together handles most of the cases. In other corner cases, you'd better format it into String rather than defining your own Interpolation.

[andrevidela]

In other corner cases, you'd better format it into String rather than defining your own Interpolation

I'm not sure I understand this correctly. The Interpolation interface is precisely here to handle corner cases where you want to format your data specially for interpolation. It's not hard to come by either: Typically record types have multiple fields that you want to show across multiple lines, but if you insert it within an interpolated string, the line breaks will mess up your formatting, so the Interpolation instance should not have any line breaks. Here is a very real example:

record HTTPRequest where
  method : String
  uri: String
  header : String
  body : String

Show HTTPRequest where
  show req = """
    method: \{req.method}
    uri: \{req.uri}
    header: \{req.header}
    body: \{req.body}
    """
Interpolation HTTPRequest where
  interpolate req = "\{req.Method} \{req.uri}"

...

-- Use show to render Requests by themselves
sendRequest : HTTPRequest -> IO ()
sendRequest req = server.send (show req)

...

-- Use interpolate to insert in other strings
parseRequest : RequestParser a => Request -> Log a
parseRequest req = case parse req of Nothing => LOG Error "could not parse \{req}"; Just v => pure v

I agree that having to type %hide interpDefault is a usability regression. Maybe the opposite would be more desirable? that is, having to import the default interpolation

import Interpolation.Default

-- now we have access to Show a => Interpolation a

This also affords is the option to backpedal without making a breaking change if we find a solution to ambigious interfaces, what do you think?

[andylokandy]

@andrevidela The users may also want to use the multiline version HTTPRequest in interpolation. I feel uncomfortable making Interpolation a format-behavior variant against Show.

To me, the first reasonable solution to your example should be to add a Display interface and to somehow control whether Show a => Interpolation a or Display a => Interpolation a to use in string literal interpolation (Rust uses {} and {:?} for that purpose).

Therefore, it leads to a design decision of Idris: How to idiomatically add more new format behavior to Idris? Currently, Idris only has two behavior Show and Pretty, and potentially the third, Interpolation. Should we learn Rust and then add a bunch of formatter interfaces, e.g. Debug, Display, Octal, Binary and more?

I think functions are more flexible and idiomatic in Idris rather than builtin formatter, so I think we should use simple functions for new format behavior. Then the Show is really an internal structure printer for developers like Debug in Rust.

To give a concrete example on top of yours:

record HTTPRequest where
  method : String
  uri: String
  header : String
  body : String

Show HTTPRequest where
  show req = """
    method: \{req.method}
    uri: \{req.uri}
    header: \{req.header}
    body: \{req.body}
    """

display : HTTPRequest -> String
display req = "\{req.Method} \{req.uri}"
...

-- Use show to render Requests by themselves
sendRequest : HTTPRequest -> IO ()
sendRequest req = server.send (show req)

...

-- Use interpolate to insert in other strings
parseRequest : RequestParser a => Request -> Log a
parseRequest req = case parse req of Nothing => LOG Error "could not parse \{display req}"; Just v => pure v

[andylokandy]

that is, having to import the default interpolation ... This also affords is the option to backpedal without making a breaking change if we find a solution to ambigious interfaces, what do you think?

Once imported Interpolation.Default into a module, you have no way to use any type that manually implements Interpolation in a string literal because of ambiguity. And you aren't even able to %hide that unnamed implementation. Which means we have to reach an agreement on whether do or not to do but can't in between.

[stefan-hoeck]

There more I read about this, the more this sounds like a code smell. Why do we have an Interpolation interface in the first place if client code is not supposed to implement it? I agree with you, @andylokandy, that the best solution would be to use explicit string conversion functions anyway. It's slightly more verbose but comes with much less mental overhead and therefore, fewer surprises. So: If users are not supposed to implement Interpolation, I'd suggest to get rid of it altogether and only allow expressions of type String in interpolation. From my own experience, this works very well.

Edit: And if this criticism sounds too harsh: Please understand, that I am very glad about your work on string interpolation and raw string literals. They are a really great and useful addition to the language. :-)

[andylokandy]

If users are not supposed to implement Interpolation, I'd suggest to get rid of it altogether and only allow expressions of type String in interpolation. From my own experience, this works very well.

@stefan-hoeck Yes! Exactly the same as my previous comment a long time ago. Anyway, I now believe a default Show a => Interpolation a also works well in many cases, especially for enums, for debugging, and for development. So I still think Interpolation is necessary but can be hidden from most users.

[gallais]

If users are not supposed to implement Interpolation,

I don't understand where this impression came from.

Adding your own implementation is only a problem if we accept the idea of adding this Show a => Interpolation a.
Which to me indicates the issue is with this overly ambiguous implementation rather than with Interpolation.

[andylokandy]

If users are not supposed to implement Interpolation,

I don't understand where this impression came from.

The idea comes from this comment

[stefan-hoeck]

If users are not supposed to implement Interpolation,

I don't understand where this impression came from.

This impression comes from the discussion in this PR. Namely:

In other corner cases, you'd better format it into String rather than defining your own Interpolation

Adding your own implementation is only a problem if we accept the idea of adding this Show a => Interpolation a. Which to me indicates the issue is with this overly ambiguous implementation rather than with Interpolation.

Agreed.