Add Text/replace builtin

[alexhumphreys]

This attempts to standardise the Text/replace builtin.

There's a few parts I wasn't sure on (eg. the B case for the test tests/parser/success/builtinsA.dhall), and there's probably plenty other things I missed so best to look over this carefully.

Also, wasn't sure how best to describe this feature in the prose sections (doc strings in prelude, Language-tour.md, etc.). I feel the need to use the phrase "substring" but Dhall has Text not String so maybe that's misleading. So if anyone has suggestions to make those descriptions more clear I'd appreciate it.

Fixes #1051.

[Gabriella439]

Looks great so far!

I think one thing we need to decide is what to do if the substring to replace is "", in order to avoid an infinite loop. Some possibilities I can think of are:

• Silently perform no replacement if the substring to replace is empty
• Return an Optional with a None result
• Require the substring to replace to be statically known at type-checking time and return a type error if empty

[alexhumphreys]

As regards "", I'd vote for the first choice of do nothing. The second choice of returning an optional seems unergonomic. The third choice seems like an odd type error, given that "non-empty string" (or non-empty list for that matter) isn't a type that exists anywhere else in the language.

Just tried ruby to see what it does in this case and it was not what I was expecting:

"foo".gsub "" "bar" == "barfbarobarobar"

... not sure we want to follow that example 😅 Though I can see a case to be made for Text/replace "" "foo" "" === "foo".

I don't feel strongly about this though, whatever ye all prefer is cool.

[alexhumphreys]

@Gabriel439 I've committed your suggested change defining normalisation in terms of recursion. I've also added a note to do nothing in the case of "" as the substring to replace, and if we decide on some other behaviour I can update this later.

[Gabriella439]

@alexhumphreys: I'm taking vacation this week, but I'll review again afterwards

[alexhumphreys]

Ah nice, enjoy the vacation! 🌴

[Gabriella439]

Could you also add a test for replacing an empty string? That way, implementations won't forget to handle that case

Other than that, this looks to me like this proposal is basically ready to move out of Draft status

[Gabriella439]

Could you move this judgement to be the first or second one? The standard has an implicit "first judgement wins" convention that we've been using when more than one judgement applies, and we want this judgment to take precedence

[alexhumphreys]

Updated.

[alexhumphreys]

@Gabriel439 I've added that empty string test. I still don't have the B case for tests/parser/success/builtinsA.dhall as I'm not sure what Text/replace gets parsed as, but aside from that it's good for me to move this out of draft status.

[sjakobi]

Isn't the normalization still way under-specified? How are composite characters supposed to be handled, for example? (I believe @Profpatsch had some opinions about that in some discussion about Text operations)

[Gabriella439]

@sjakobi: I'd propose doing replacement at the grapheme level, as suggested by this test:

dhall-lang/Prelude/Text/replace.dhall

Line 12 in 595c8ca

let example2 = assert : replace "👨" "👩" "👨‍👩‍👧‍👦" ≡ "👩‍👩‍👧‍👦"

… and for correctly handling composite characters I'd suggest performing the replace if the "needle" and the prefix are both canonically equivalent, meaning that they have the same normalization form, specifically Normalization Form C.

[sjakobi]

@Gabriel439 Sounds good to me!

[alexhumphreys]

@Gabriel439 @sjakobi I updated this with a note on using NFC. Well, I pretty much just took your comment from above. Does this need more detail or would that be clear enough?

[Gabriella439]

Could you also add this as one of the test cases in the standard test suite?

[alexhumphreys]

Yep, updated. Should I leave this in the prelude? Just wondering how easy this will be for all implementations, since most users importing the prelude won't need this particular replacement.

[Gabriella439]

I think it is also worth keeping in the Prelude since this is useful documentation for the end user. These examples will also show up in the generated docs

[Gabriella439]

@alexhumphreys: I have a PR open with all of my suggested changes in: alexhumphreys#1

I decided to skip handling normalization for now (and adding a test making that explicit). I can standardize support for Unicode normalization in a separate proposal, to keep this pull request simpler.

[Gabriella439]

I also have a matching change to the Haskell implementation up here: dhall-lang/dhall-haskell#2063

[alexhumphreys]

@Gabriel439 thanks for the PR, those beta normalisation rules are a lot clearer. It also thought me a bit about string interpolation: didn't know it would get normalised under a lambda binding before the lambda is applied.

Splitting the Unicode handling to a different PR is cool too. Would let example2 = assert : replace "👨" "👩" "👨‍👩‍👧‍👦" ≡ "👩‍👩‍👧‍👦" still remain in the prelude for this PR? I think the output of that wouldn't change between NFC and NFD normalisation, so it should be ok.

[Gabriella439]

@alexhumphreys: I think that example would be the same regardless of how we handle normalization

[sjakobi]

LGTM apart from one more wibble. Thanks! :)

[Gabriella439]

@alexhumphreys: You should be clear to merge this

[alexhumphreys]

@Gabriel439 sweet! Any 3 day waiting period or can I just hit the button?

[Gabriella439]

@alexhumphreys: Since you don't have a majority of approvals but you also don't have a majority of disapprovals then the policy is 7 days since the PR was ready (i.e. not a draft PR) and 1 day since last code change. For more details, see: https://github.com/dhall-lang/dhall-lang/blob/master/.github/CONTRIBUTING.md#how-do-changes-get-approved

[alexhumphreys]

Ah cool, so it should be good to be merged. Looks like I don't have write access so maybe one of ye wants to hit the button? Also there's 25 commits in this PR now, do ye have a policy of squashing commits or should I go in and tidy up the history a bit?

[philandstuff]

This repo enforces squash-on-merge. We should get you the commit bit so you can merge yourself 👍🏻

[philandstuff]

@alexhumphreys I’ve granted you write access now, check your email

[alexhumphreys]

Sweet! Thanks @philandstuff, and everyone else too for helping on this 🙂

[Gabriella439]

@alexhumphreys: Thank you, too! Also, now that this is merged you can submit an invoice here for $200 and one of us will approve it: https://opencollective.com/dhall/expenses/new

[alexhumphreys]

Thanks, but it's ok! I've been meaning to donate to that Dhall fund so consider this a contribution 🙂

[basile-henry]

Sorry, I'm a bit late for a review. I just have a question as I am attempting to implement this in dhall-rust. 😅

[basile-henry]

I don't really understand how the haystack can be abstract. Don't we want to replace occurrences of the needle in the abstract section too? i.e. What happens if y is the string "a"?

[Gabriella439]

@basile-henry: Oh, I see what you mean. Allowing the haystack to be abstract means that β-reduction is no longer confluent. For right now, just ignore that test and I can put up a change to require the haystack to be non-abstract before further reduction can occur.