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.