Better handling of JSON sums

[enolan]

We have a bunch of Packer files at work that have a bunch of redundancy between them, so I thought this was a good use case for Dhall. It turned out to be more trouble than it's worth though. There's a provisioners field that contains a list of instructions for provisioning VMs using various tools. E.g.:

{
  // other stuff
  "provisioners": [
    {
      "type": "shell",
      "inline": ["echo foo"]
    },
    {
      "type": "file",
      "source": "app.tar.gz",
      "destination": "/tmp/app.tar.gz"
    }
  ]
}

There are lots of kinds of provisioners, distinguished by the type field. The natural Dhall encoding is something like < File : { source: Text, dest: Text} | Shell : List Text>, but if I want to convert that to JSON that Packer will accept, the output type has to be {type: Text, source: Optional Text, destination: Optional Text, inline: Optional Text}. That gets worse as I add support for more provisioners. Writing the provisioner to JSON function is ugly too:

   let provisionerEmpty = {
         source = [] : Optional Text,
         destination = [] : Optional Text,
         inline = [] : Optional (List Text)}
in let provisioner_to_json = \(p: Provisioner) ->
         merge
         {File = \(ps: {source: Text, dest: Text}) -> provisionerEmpty // {type = "file", source = [ps.source] : Optional Text, destination = [ps.dest] : Optional Text},
          Shell = \(lines: List Text) -> provisionerEmpty // {type = "shell", inline = [lines] : Optional (List Text)}
         }
         p in ...

It'd be great if there was a nice way of generating JSON sum types.

[Gabriella439]

@enolan: Could you sketch what the ideal syntax would be for you for defining provisioners in a type-safe way?

[enolan]

That's a very good question. I've been thinking about it on and off since you asked.

The most "obvious" solution is a separate type constructor for JSON sums. Something like this:

   let Provisioner = constructors (JSONSum "type" {
       shell : { inline : List Text },
       file : { source : Text, destination : Text }
     })
in { provisioners = [
     Provisioner.shell { inline = ["echo foo"] },
     Provisioner.file { source = "app.tar.gz", destination = "/tmp/app.tar.gz" }
   }

If consumers of the dhall library could add primitives you could get this without adding anything JSON specific to the core language. If you wanted JSONSum to be a function instead of a primitive you'd need dependent types, as the map of tag names to record types is a value.

It's also worth noting that some JSON formats have the tag, then associated values in a child object e.g.

{ "provisioners": [
    { "type": "shell",
      "params": {
        "inline": ["echo foo"]
      }
    },
    { "type": "file",
      "params": {
        "source": "app.tar.gz",
        "destination": "/tmp/app.tar.gz"
      }
    }
  ]
}

That would need a separate type constructor.

[Gabriella439]

So we might not be able to do this at the language level (this seems a bit JSON-specific) but I do think we can add support for something like this in dhall-to-json (similar to existing support for encoding homogeneous maps)

Currently, dhall-to-json encodes sum types to JSON by stripping the tag entirely, but it would be a very easy change to add support for including the tag as a field (either inline within the child record if it is a record or wrapped in a new record) if it notices a certain pattern.

The UX I have in mind is not to use a command line option (since that requires specifying this behavior globally which might not work). Instead, you would wrap the sum type in some magic record specifying how to encode it to JSON, like this:

{ tagField = "type"
, nesting = < NestedField = "value" | Inline : {} >
, contents = < Left = 1 | Right : Bool >
}

... and it would translate that to this JSON:

{ "type": "Left", "value": 1 }

So then the UX for your example would be something like:

    let map =
          https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map 

in  let Provisioner =
          < shell :
              { inline : List Text }
          | file :
              { source : Text, destination : Text }
          >

in  let provisioner = constructors Provisioner

    -- NOTE: The `Tagged` and `Nesting` types can be provided by a JSON
    -- subset of the Dhall Prelude, similar to:
    --
    -- https://github.com/dhall-lang/Prelude/pull/5
in  let Tagged =
            λ(a : Type)
          → { tagField :
                Text
            , nesting :
                < Inline : {} | NestedField : Text >
            , contents :
                a
            }

in  let Nesting = < Inline : {} | NestedField : Text >

in  let nesting = constructors Nesting

in  let wrap
        : Provisioner → Tagged Provisioner
        =   λ(x : Provisioner)
          → { tagField = "type", nesting = nesting.Inline {=}, contents = x }

in  { provisioners =
        map
        Provisioner
        (Tagged Provisioner)
        wrap
        [ provisioner.shell { inline = [ "echo foo" ] }
        , provisioner.file
          { source = "app.tar.gz", destination = "/tmp/app.tar.gz" }
        ]
    }

[enolan]

That sounds like it would work.

[Gabriella439]

@enolan: Alright, I have a pull request up with support for this here:

https://github.com/dhall-lang/dhall-json/pull/38

Give that a try and let me know if it works for you

[Gabriella439]

@enolan: Here's the matching change to the Prelude to make working with this feature easier:

https://github.com/dhall-lang/Prelude/pull/6

I didn't add any wrap-like utilities yet because I wasn't sure how to add a utility that was sufficiently general that was any simpler than just creating the record.