How to represent the following JSON in Dhall?

Question

I am using the following JSON to represent our infrastructure. This is a greatly simplified version.

{
  "us-east-1": {
    "qa": {
      "etcd": {}
    }
  },
  "eu-central-1": {
    "dev": {
      "etcd": {}
    }

  },
  "eu-west-1": {
    "prod": {
      "etcd": {}
    }
  }
}

This can be mapped to folders and it is easy to handle from code.

#!/usr/bin/env python
import json
import os, sys

with open('infrastructure.json', 'r') as read_file: infra = json.load(read_file)

regions = infra.keys()
for region in regions:
    stages = infra[region].keys()
    for stage in stages:
        apps = infra[region][stage].keys()
        for app in apps:
            os.makedirs(os.path.join('infra', region, stage, app), 0o750, exist_ok=True)
            print('region: {}, stage: {}, app: {}'.format(region, stage, app))

However, I would like to generate this file using Dhall to restrict the possible keys to lists.

Dhall has support for this:

let AwsRegions : Type = < us-east-1 | eu-central-1 | eu-west-1 >
let Stages : Type = < dev | qa | prod >
let Applications : Type = < etcd | postgresql | hadoop >

The only problem is that I could not find support to have a record key as an empty type, only the values can be restricted to those.

This makes me have our infra the following way:

let infrastructure : 
List {  region: AwsRegions, stage: Stages, 
        applications: List Applications } =
[ {     region = AwsRegions.us-east-1, 
        stage =  Stages.dev,
        applications = [ 
            Applications.hadoop, 
            Applications.etcd ] },
    {   region = AwsRegions.eu-west-1, 
        stage =  Stages.dev,
        applications = [ 
            Applications.hadoop, 
            Applications.etcd ] },
    {   region = AwsRegions.eu-central-1, 
        stage =  Stages.dev,
        applications = [ 
            Applications.hadoop, 
            Applications.etcd ] },
    {   region = AwsRegions.eu-west-1, 
        stage =  Stages.qa,
        applications = [ 
            Applications.hadoop, 
            Applications.etcd ] },
    {   region = AwsRegions.eu-west-1, 
        stage =  Stages.prod,
        applications = [ 
            Applications.hadoop, 
            Applications.etcd ] } ]
in infrastructure

The generated JSON is a bit harder to handle from code and I cannot easily reference subset of our infra like with the other representation.

Is there a way to have keys like enums (a union for empty types) with Dhall?

Answer 1

This would be the idiomatic way to generate nested JSON records whose keys were restricted to enums:

let keyValue =
        λ(k : Type)
      → λ(v : Type)
      → λ(mapKey : k)
      → λ(mapValue : v)
      → { mapKey = mapKey, mapValue = mapValue }

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

let Application = < etcd | postgresql | hadoop >

let Applications = Prelude.Map.Type Application {}

let application = λ(application : Application) → keyValue Application {} application {=}

let Stage = < dev | qa | prod >

let Stages = Prelude.Map.Type Stage Applications

let stage = keyValue Stage Applications

let AwsRegion = < us-east-1 | eu-central-1 | eu-west-1 >

let AwsRegions = Prelude.Map.Type AwsRegion Stages

let awsRegion = keyValue AwsRegion Stages

in  [ awsRegion AwsRegion.us-east-1
        [ stage Stage.dev
             [ application Application.hadoop
             , application Application.etcd
             ]
        ]
    , awsRegion AwsRegion.eu-west-1
        [ stage Stage.dev
             [ application Application.hadoop
             , application Application.etcd
             ]
        , stage Stage.qa
             [ application Application.hadoop
             , application Application.etcd
             ]
        , stage Stage.prod
             [ application Application.hadoop
             , application Application.etcd
             ]
        ]
    , awsRegion AwsRegion.eu-central-1
        [ stage Stage.dev
            [ application Application.hadoop
            , application Application.etcd
            ]
        ]
    ]

... which renders as the following JSON:

$ dhall-to-json/dhall-to-json --file /tmp/test/example.dhall 
{
  "eu-central-1": {
    "dev": {
      "etcd": {},
      "hadoop": {}
    }
  },
  "eu-west-1": {
    "dev": {
      "etcd": {},
      "hadoop": {}
    },
    "prod": {
      "etcd": {},
      "hadoop": {}
    },
    "qa": {
      "etcd": {},
      "hadoop": {}
    }
  },
  "us-east-1": {
    "dev": {
      "etcd": {},
      "hadoop": {}
    }
  }
}