Sum type value equal predicate

#1

How would you compare two sum type value? For example I’m trying to model a group of object using a sum type like so:

let Group = < backend | frontend >

let Object = { name : Text, group : Group }

let objects =
      [ { name = "db01", group = Group.backend }
      , { name = "db02", group = Group.backend }
      , { name = "lb01", group = Group.frontend }
      ]

let FrontEnds =
      https://prelude.dhall-lang.org/v14.0.0/List/filter
        Object
        (     \(obj : Object)
          ->  merge { backend = False, frontend = True } obj.group
        )

in  FrontEnds objects

Unfortunately this isn’t practical as each time a group is added, all the merge calls need to be updated. Wouldn’t it make sense to support such predicate: obj.group === Group.frontent ? I was hoping the text manipulation function thread would enable a Text/Equal function to help with that topic, but perhaps a sum type equal test would be more adequat?

#2

@tristanC: I view equality for unions as a special case of a wildcard pattern match (where you return True for the desired case and False for the wildcard case). So I think it’s worth deciding if we want to support wildcard pattern matches or not.

#3

FYI Gabriel described a code pattern for union equality here.

#4

I was not aware of this idea. Would it look like merge foo { somefield = True, _ = False } ? That sounds like a great idea to me.

#5

The code pattern for union equality looks better, and having a wildcard pattern match would be even better. However it seems like we have to keep a list of equality function in sync for all the possible union value.

In the initial model I pasted above, there is an extra challenge where I need to produce an inventory file that contains all the objects per group like so:

children:
  backend:
    db01:
    db02:
  frontend:
    lb01:

Not sure how this is usually done in haskell, or other language having such type system, but the way I solved that challenge required to also maintain a list of all the union values. In the end, I wrote a script to generate such code from the initial Group type:

let default = { backend = False, frontend = False }

let Groups =
      [ { value = Group.backend
        , test = \(group : Group) -> merge (default // { backend = True }) group
        }
      , { value = Group.frontend
        , test =
            \(group : Group) -> merge (default // { frontend = True }) group
        }
      ]

I think it would be more ergonomic if dhall could automatically provide equality and iterator for union values, at least when they are used as enum. Note that wouldn’t be necessary if a Text/equal function existed, however that would be drawback as Text is prone to typo.

#6

Actually, the code pattern for union equality @sjakobi linked above renders my script less useful as the pattern makes it easier to maintain the code. While doing the change I also found a little trick to get the list of all values: instead of using a List, I can use a Record and consume it using the toMap function. That enables using a dumb merge function to ensure all the handler are present :slight_smile:

In the end, when adding (or removing) an element from the union, I need two other changes:

  • Add to the default record an attribute to False.
  • Add an handler that contains the value and the equality test function.

With a wildcard pattern match I would only need the latter. I still think it would be more ergonomic if dhall could automatically takes care of that (equality and iterator). But I can live with the current implementation, thanks a lot for the discussion!

For what its worth, here is the change I wrote to use the code pattern for union: Groups.dhall.

#7

Handling equality is a difficult problem for language design in general. IIRC, this problem led to the invention of typeclasses in Haskell as an elegant way to solve it.

There are two ways I could imagine solving this problem in dhall: one is having the compiler magically know how to compare values, and some typeclassy way of restricting polymorphism to types that can be compared; two would be a mechanism, like derive in Haskell, that produces a function eqT: T -> T -> Bool on-demand for a given type, and then we can pass this function around and use it.
Both solutions have a serious limitation however: what if I want to define a type of rational numbers as pairs of numbers ? Then I’d want to write a custom equality function. The problem arises directly with the first solution, because it gives us only one notion of equality and that’s it. For the second solution, we can easily use our custom equality function, but what if I want to derive equality for a pair of rationals ? Then again I need a way to tell the compiler to use my custom function.

If we don’t want to allow custom comparison functions, then the problem looks a bit simpler. However It would limit dhall’s abstraction capabilities, which I find sad.
If we do want custom comparison functions, then a potential solution I was thinking about would be ML-style modules. Instead of passing around a pair of integers, I would pass around a record Rational : { T : Type, eq : Rational.T -> Rational.T -> bool }. So we’d need dependent sums (I’ve been wanting those for a while). On top of that we could build a deriving mechanism that constructs appropriate such eq functions automatically.

I don’t see any simple way around this problem. What do you guys think ? Do we want to support this ? Any other approaches that could work ?

#8

@Nadrieril: One of the reasons I drag my feet on language support for equality is because a lot of cases where it’s requested can be due to trying to convert a weakly typed data representation back into a strongly typed one.

In general, when designing the language I try to encourage starting from a strongly typed representation and then “going downhill” to convert that to more weakly-typed representations, rather than the other way around.

For example, toMap is an example of a keyword that promotes this idiom, where it starts from a strongly-typed representation (i.e. a record) and then “goes downhill” to convert to a weakly typed representation.

Revisiting the original request, the objects variable stores a weakly-typed representation where the front-ends and backends have been mixed together and the way I read the request is to recover the strongly-typed representation where frontends and backends are separated from the weakly-typed representation where they have already been mixed.

However, we could have refactored the code to store the various groups separately (a strongly-typed representation) and then convert to the weakly-typed representation at the end, rather than try to do it the other way around:

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

let Group = < backend | frontend >

let Object = { name : Text, group : Group }

let frontends = [ "db01", "db02" ]

let backends = [ "lb01" ]

let adapt =
        λ(group : Group)
      → Prelude.List.map
          Text
          { name : Text, group : Group }
          (λ(name : Text) → { name = name, group = group })

let objects =
        adapt Group.backend backends
      # adapt Group.frontend frontends

in  { frontends = frontends, backends = backends, objects = objects }
#9

The way I dealt with this was through the following idiom:

let Union =
  let Union = < Foo | Bar : Text >
  let equals = 
    { foo = 
      merge
      { Foo = True
      , Bar = \(_ : Text) -> False
      }
      union
    , bar = \(union : Union) ->
      merge
      { Foo = False
      , Bar = \(_ : Text) -> True
      }
      union
    }
  in
  { Type = Union
  , Foo = Union.Foo
  , Bar = \(value : Text) -> Union.Bar value
  , equals = equals
  }
let example-usage =
    { equals = 
       { foo = assert : Union.equals.foo Union.Foo == True
       , bar = assert : Union.equals.bar (Union.Bar "placeholder") == True
       , false = assert : Union.equals.bar Union.Foo == False
      }
    }
in Union

Wildcard matches would help as the union gets larger, but at least all of the merge calls are grouped with the original sum type such that they only need to be updated in one place.

#10

A little anecdote

I looked into Dhall again recently, since it seemed to me like the tooling got a lot better over the last year. I mentioned it to my colleague, who pitched me a toy challenge:

What if, for example I said:

Variable A, Values 1, 2, 3
Variable B, Values 4, 5, 6
Variable C, Values 7, 8, 9
Variable D, Values 10, 11, 12

When selecting any value for a variable, cannot select any other value for that variable

When select A1, always force add B4
When select B5, force exclude all values of variable C, and force exclude D11
When select D10, may select C9
When select D12, force select C8 and force select A1

Can it evaluate the configuration statement: “Use this module for all cases except when D11 is selected”

Now, there’s some debate about whether that’s well defined, but that’s okay! Software requirements are ill defined all the time, and type systems help us find out where the contradictions are, so I just dove in.

let A = < A1 | A2 | A3 >

let B = < B4 | B5 | B6 >

let C = < C7 | C8 | C9 >

let D = < D10 | D11 | D12 >

let Config = { a : Optional A, b : Optional B, c : Optional C, d : Optional D }

let empty = { a = None A, b = None B, c = None C, d = None D }

let examplePartial = { a = A.A1, b = None B, c = None C, d = D.D10 }

let isValid : Config -> Bool = <<validation logic>>

let fillUnderValidityConstraints : Config -> Optional Config = <<constrain partial config, or return
    failure>>

in fillUnderValidityConstraints examplePartial

But now I ran into exactly this issue. Trying to compare directly of course told me that == was not permitted for unions. So I tried merge:

let ruleA = {A1 = \(b: B) -> isB4, A2 = \(b:B) -> True, A3 = \(b:B) -> True}

But without wildcards I was starting down the barrel of a lot of boilerplate.

So…what should I do in a situation like this?

  • Am I not taking advantage of existing language features?
  • Am I using Dhall for the wrong kind of application?
  • Is there a better way to “start with a strongly type representation” in this case?
  • Should I wait for additional language features?
#11

The impression I get is that most of the solutions here are converging on adding language support for wildcards. It seems like something we could add pretty straightforwardly to the language by reserving a special label in the record (i.e. _) for wildcard matches, and disallowing that label for union alternatives

3 Likes
#12

@Nadrieril created an issue to track this in the dhall-lang repository: