Text/replace on interpolated text

[basile-henry]

This change to the beta normalization rules ensures that the normalization stays consistent.

The current haskell implementation has this weird behaviour:

➜ dhall repl
Welcome to the Dhall v1.35.0 REPL! Type :help for more information.
⊢ :let f = \(x : Text) -> Text/replace "a" "b" "a ${x} a"

f : ∀(x : Text) → Text

⊢ f "a"

"b a b"

⊢ let g = \(x : Text) -> Text/replace "a" "b" "a ${x} a" in g "a"

"b b b"

As @Gabriel439 suggested in #1065 an alternative rule could be:

require the haystack to be non-abstract before further reduction can occur

That would definitely be simpler to implement, but maybe not as strongly normalising as it could be.
Is there anything else I need to change? Should this change be documented somehow?

EDIT:
As @Nadrieril pointed out, Gabriel's suggestion really is the only rule possible here. I changed this PR to implement this suggestion instead! 😄

[Nadrieril]

I believe that "require the haystack to be non-abstract before further reduction can occur" is the only sensible rule here. For example in \(x : Text) -> Text/replace "aa" "b" "a${x}", we don't know if replacement will occur without knowing x, nor can we proceed partially without complicated analysis of the overlap between the needle and what we know about the haystack.

[basile-henry]

Good point, I didn't think about this case. 😅 I will edit the changes to the spec to reflect this tomorrow!

[basile-henry]

There is one slightly different rule possible. If the needle is empty, then the haystack does not need to be fully evaluated.

So:

Text/replace ""

Could be normalized to:

\(_replacement : Text) \(haystack : Text) -> haystack

But that goes against "builtins are fully saturated". So maybe just this:

Text/replace "" replacement haystack

Is normalized to:

haystack

Regardless of whether haystack is in normal form or not.

Is this something we might want?

[philandstuff]

This special case feels like pretty low value, I’d rather stick with the general rule for all cases.

[Nadrieril]

While you're at it, could you also add a test for \(x : Text) -> Text/replace "a" x "aaa" and λ(x : Text) → Text/replace "aa" "b" "a${x}"?

[Gabriella439]

Thank you for doing this! 🙂

[Nadrieril]

As per the rules, I believe you can now merge this, since there are no objections

[basile-henry]

Alright great! I've updated the branch. I don't think I have write access in this repo though, so someone else will have to merge this PR. 😄

[Gabriella439]

@basile-henry: I just added you to the repository

[basile-henry]

Great, thanks! 😄

[Gabriella439]

You're welcome! 🙂