Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Discussion: Text equality #164

Closed
f-f opened this issue May 29, 2018 · 24 comments
Closed

Discussion: Text equality #164

f-f opened this issue May 29, 2018 · 24 comments
Labels

Comments

@f-f
Copy link
Member

@f-f f-f commented May 29, 2018

The readme of this repo mentions:

Dhall is a very minimal programming language. For example: you cannot even compare strings for equality.

The reason for this is detailed in this comment:

The main reason for forbidding Text equality comparisons is to prevent people from parsing Text values at all, in order to encourage them to use more structured data types instead.

However, the problem I have at hand (emitting a different config depending on the value of an envvar) is currently impossible to implement without string equality.
So, I propose we add the == operator for Text, with the following signature:

(a : Text)  (b : Text)  Bool

I think the value added from it (since not having it prevents from solving certain problems) is way bigger than the potential increase in complexity.

Thoughts?

/cc @Gabriel439

@f-f f-f changed the title String equality Discussion: Text equality May 29, 2018
@ocharles

This comment has been minimized.

Copy link
Member

@ocharles ocharles commented May 29, 2018

This sounds quite specific to your problem, so you can simply supply ∀(a : Text) → ∀(b : Text) → Bool as an argument in your program, and do the string equality there. It doesn't have to be added to Dhall itself. You could also postulate its existence by using typeCheckWith and friends.

@Profpatsch

This comment has been minimized.

Copy link
Member

@Profpatsch Profpatsch commented May 29, 2018

So, I propose we add the == operator for Text, with the following signature:

Uh, what kind of comparison do you want to set it to?
Should strings be compared byte-wise? What about Unicode Normalization?

so you can simply supply ∀(a : Text) → ∀(b : Text) → Bool

This is also the more general solution, because you can decide on a per-use-case basis what equality on text means.

@Gabriel439 Gabriel439 closed this May 29, 2018
@Gabriel439 Gabriel439 reopened this May 29, 2018
@Gabriel439

This comment has been minimized.

Copy link
Contributor

@Gabriel439 Gabriel439 commented May 29, 2018

Sorry, I fat-fingered the close button on my phone while reading this

@Gabriel439

This comment has been minimized.

Copy link
Contributor

@Gabriel439 Gabriel439 commented May 29, 2018

@f-f: Environment variables can store structured Dhall expressions. I'd need more context here, but I'd still prefer not to include support for string equality in order to avoid stringly typed programming.

More generally, I prefer to push strong typing requirements further upstream rather than push weakly typed parsing logic further downstream. The goal is to carve out a strongly typed pipeline that pushes parsing and input validation to the edge of the system (and to keep pushing that edge outward). Reintroducing parsing into that pipeline compromises most of the guarantees of strong typing if it becomes idiomatic because then most programs will begin to return Optional values and thus be susceptible to runtime failures.

@Gabriel439

This comment has been minimized.

Copy link
Contributor

@Gabriel439 Gabriel439 commented May 29, 2018

I also want to note that we shouldn't reject this idea on the basis of the difficulty of comparing Unicode strings for equality. The Unicode standard does define how to do this and we can delegate the responsibility of doing that correctly to Unicode implementations in each respective language binding.

@ocharles

This comment has been minimized.

Copy link
Member

@ocharles ocharles commented May 29, 2018

@f-f

This comment has been minimized.

Copy link
Member Author

@f-f f-f commented May 29, 2018

Let me prelude by saying that I agree with all of you on the fact that Dhall does not need string equality, mostly exploring the space of possibilities here :)
(also, future reference. Someone will have the same question at some point, so having a thread about it is likely going to be useful)

@ocharles @Gabriel439
Thanks for suggesting the envvar solution, in the end my current problem is going to be solved by putting a Bool in a separate var and branching on that.
However, to cover most of the envvar-related-branching-problems I feel that #163 is most likely fundamental to have.

@ocharles @Profpatsch
I agree with @Gabriel439 here that the problem is not really the Unicode Normalization or not, and more generally there should not be an effort to encompass all the usecases, as long as there is a clear cut. E.g. I'd go for straight byte comparison (so not-normalized, not-white-collapsed, case-sensitive, etc).
But the real point (that is hard to disagree with) is in fact this:

avoid stringly typed programming

@aleator

This comment has been minimized.

Copy link

@aleator aleator commented Jun 5, 2018

How about having equality for sum types, and for them only? You already can do it by yourself in dhall, but ergonomics are really bad.

@Gabriel439

This comment has been minimized.

Copy link
Contributor

@Gabriel439 Gabriel439 commented Jun 7, 2018

@aleator: Are you sure you want to use equality for large sum types, though? I'd assume that pattern matching with something like a wild-card match for cases that you are not interested in would be more appropriate than testing for equality on constructors one-at-a-time

@aleator

This comment has been minimized.

Copy link

@aleator aleator commented Jun 7, 2018

@Gabriel439 Well, given a choice, I would take wildcards in merge over equalities. I just had the above use case in mind.

Having either would also be a step towards a lookup function for association lists (by labeling them with sums), which I had previously wanted.

@Gabriel439

This comment has been minimized.

Copy link
Contributor

@Gabriel439 Gabriel439 commented Jun 7, 2018

@aleator: So then I think the main thing is coming up with a way to do wild-card pattern matches.

One way to do so is to have some keyword analogous to constructors (maybe wildcard) that produces a record of handlers that all return the same result. Then you could selectively override the behavior of certain handlers, like this:

    let handlers = wildcard "foo" < A : {} | B : {} | C : {} >

in  handlers // { A = λ(_ : {})  "bar" }

... which would default to "foo" and return "bar" for the A constructor

@aleator

This comment has been minimized.

Copy link

@aleator aleator commented Jun 7, 2018

@Gabriel439 that seems like a nice way,. Another would be to have another parameter for merge (or some similar keyword) which would possibly be easier to optimize.

Third choice would be to use some special field label for the wildcard, but that seems like a bad idea.

It should be noted that this is not enough to implement equality which would be useful for lookup kind of things. However, similar approach could also synthesize equality functions.

@blast-hardcheese

This comment has been minimized.

Copy link

@blast-hardcheese blast-hardcheese commented Jun 20, 2018

I've run into this in dhall-terraform as well, where structured data bubbles up to an association list at the top level where the keys must be unique.

As the consumers should not need to know about the implementation details of each of the resources they are consuming, I find that not having string comparison here breaks encapsulation of concerns, mandating that users explicitly maintain this association list themselves, which is exactly what drew me to Dhall in the first place.

@Gabriel439

This comment has been minimized.

Copy link
Contributor

@Gabriel439 Gabriel439 commented Jun 20, 2018

@blast-hardcheese: One idea that I floated in #169 (comment) is that we could add support for converting a record to an association list. That way the record can enforce uniqueness of keys and allow a way to access fields by key name but then you can later convert the record to a list of key-value pairs for anything expecting that

Would that work for you?

@blast-hardcheese

This comment has been minimized.

Copy link

@blast-hardcheese blast-hardcheese commented Jun 25, 2018

@Gabriel439 I believe it would. My understanding of the problem scope is as follows:

Given the current state of the world, the following structure:

    let struct1 = { variables = [ { key = "foo", value = "something" } ] }

in  let struct2 =
          { variables =
              [ { key = "foo", value = "something" }
              , { key = "bar", value = "something else" }
              ]
          }

in  struct1.variables # struct2.variables

results in

[{"value":"something","key":"foo"},{"value":"something","key":"foo"},{"value":"something else","key":"bar"}]

where the consuming API expects uniqueness for [].key. This is currently not able to be satisfied due to duplicates.

From what I get out of that comment, you'd convert

    let struct1 = { variables = { foo = "something" } }

in  let struct2 = { variables = { foo = "something", bar = "something else" } }

in  toAssociationList (struct1.variables /\ struct2.variables)

into

[ { key = "foo", value = "something" }
, { key = "bar", value = "something else" }
]

which would indeed solve my problems.

@f-f

This comment has been minimized.

Copy link
Member Author

@f-f f-f commented Oct 30, 2018

As the original author of the issue I think it now accomplished its original purpose - it is informative when the topic comes up again and can be cross-linked from other places. I guess if it comes up again often enough we should port some of this content to a FAQ entry.

So I'll close this, and add the "discussion" label so that it's easier to find.

@f-f f-f closed this Oct 30, 2018
@gvolpe

This comment has been minimized.

Copy link

@gvolpe gvolpe commented Jan 15, 2019

Hi, I'm quite new to using dhall and I stumbled across this issue. I read all the comments but still it is not very clear on what's the alternative to this. I have a very simple case:

let makeConfig = λ(env : Text)   
  { uri : Text }

The value of uri depends on the value of env . How can I achieve this? I only have two possible values.

@jneira

This comment has been minimized.

Copy link
Collaborator

@jneira jneira commented Jan 15, 2019

Usually it is modeled as a Union type with two values:

let Env = < Val1 : {} | Val2 : {} >
let makeConfig =  λ(env : Env)   { uri = "whatever" }
in makeConfig ( Env.Val1 {=} )

A more complete example would be:

let Env = < Val1 : {} | Val2 : {} >
let makeConfig =
    λ(env : Env)  
      let uri = merge { Val1 = λ(x : {})  "uri1", Val2 = λ(x : {})  "uri2" } env
      in { uri = uri }
in makeConfig ( Env.Val1 {=} )
@gvolpe

This comment has been minimized.

Copy link

@gvolpe gvolpe commented Jan 16, 2019

Thanks a lot @jneira , that works for me! 👍

@jneira

This comment has been minimized.

Copy link
Collaborator

@jneira jneira commented Jan 16, 2019

You are welcome!

@daddykotex

This comment has been minimized.

Copy link

@daddykotex daddykotex commented Feb 12, 2020

Here is a similar problem I faced. I'm writing some Dhall code to generate a HAProxy configuration file. It's working well and I had one issue. I'm trying to compare two union type and I could not figure it out

I wrote two snippet of code to show my issue. The first one is the problem I have and the second one is an alternative implementation where I don't have the problem but achieve the same result. I think it can be a great resource for someone with the same problem.

Problem:

let filter = https://prelude.dhall-lang.org/List/filter

let any = https://prelude.dhall-lang.org/List/any

let Zone
    : Type
    = < Prod | Sandbox >

let Service
    : Type
    = { name : Text, availableInZones : List Zone }

let services
    : List Service
    = [ { name = "service1", availableInZones = [ Zone.Prod, Zone.Sandbox ] }
      , { name = "service2", availableInZones = [ Zone.Sandbox ] }
      ]

let serviceByZone
    : Zone  List Service
    =   λ(zone : Zone)
       let zoneEqual = λ(zone : Zone)  True

        let checkZoneAvailability
            : Service  Bool
            = λ(service : Service)  any Zone zoneEqual service.availableInZones

        in  filter Service checkZoneAvailability services

in  serviceByZone Zone.Prod

The alternate solution:

let filter = https://prelude.dhall-lang.org/List/filter

let Zone
    : Type
    = < Prod | Sandbox >

let Service
    : Type
    = { name : Text, availableIn : Zone  Bool }

let allZone = λ(zone : Zone)  merge { Prod = True, Sandbox = True } zone

let sandboxOnly = λ(zone : Zone)  merge { Prod = False, Sandbox = True } zone

let services
    : List Service
    = [ { name = "service1", availableIn = allZone }
      , { name = "service2", availableIn = sandboxOnly }
      ]

let serviceByZone
    : Zone  List Service
    =   λ(zone : Zone)
       let checkZoneAvailability
            : Service  Bool
            = λ(service : Service)  service.availableIn zone

        in  filter Service checkZoneAvailability services

in  serviceByZone Zone.Prod

In the end I prefer the alternative solution, but it might be interesting to understand how I could fix the problem.

@Gabriel439

This comment has been minimized.

Copy link
Contributor

@Gabriel439 Gabriel439 commented Feb 13, 2020

@daddykotex: In general, it is possible (albeit verbose) to implement an equality function on a union like Zone, like this:

let Zone = < Prod | Sandbox >

let isProd = λ(zone : Zone)  merge { Prod = True, Sandbox = False } zone

let isSandbox = λ(zone : Zone)  merge { Prod = False, Sandbox = True } zone

let Zone/equals =
        λ(l : Zone)
       λ(r : Zone)
       isProd l && isProd r || isSandbox l && isSandbox r

in  Zone/equals

For a larger number of alternatives, you can reduce the boilerplate by using a few tricks:

let Prelude = https://prelude.dhall-lang.org/package.dhall

let T = < A | B | C | D | E | F >

let handlers =
      { A = False, B = False, C = False, D = False, E = False, F = False }

let isA = \(t : T) -> merge (handlers // { A = True }) t

let isB = \(t : T) -> merge (handlers // { B = True }) t

let isC = \(t : T) -> merge (handlers // { C = True }) t

let isD = \(t : T) -> merge (handlers // { D = True }) t

let isE = \(t : T) -> merge (handlers // { E = True }) t

let isF = \(t : T) -> merge (handlers // { F = True }) t

let {- Useful helper function to reduce repetition when defining the `*/equals`
       function
    -}
    makeEquals
    : forall (a : Type) -> List (a -> Bool) -> a -> a -> Bool
    =     \(a : Type)
      ->  \(predicates : List (a -> Bool))
      ->  \(l : a)
      ->  \(r : a)
      ->  let apply = \(predicate : a -> Bool) -> predicate l && predicate r

          in  Prelude.Bool.or
                (Prelude.List.map (a -> Bool) Bool apply predicates)

let T/equals
    : T -> T -> Bool
    = makeEquals T [ isA, isB, isC, isD, isE, isF ]

let example0 = assert : T/equals T.A T.A === True

let example1 = assert : T/equals T.A T.B === False

in  T/equals
@daddykotex

This comment has been minimized.

Copy link

@daddykotex daddykotex commented Feb 13, 2020

Thanks @Gabriel439

It's good learning material, thanks for the lengthy explanation

@Gabriel439

This comment has been minimized.

Copy link
Contributor

@Gabriel439 Gabriel439 commented Feb 13, 2020

@daddykotex: You're welcome! 🙂

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
9 participants
You can’t perform that action at this time.