How to type a heterogeneous list in dhall?

Question

I'm using Dhall to generate a Yaml file for github action. In GH Action, you can specify a matrix to generate multiple cases (e.g. combination of Scala version and project name). But you can also specify combination to exclude.

For example:

runs-on: ${{ matrix.os }}
strategy:
  matrix:
    os: [macos-latest, windows-latest, ubuntu-18.04]
    node: [8, 10, 12, 14]
    exclude:
      # excludes node 8 on macOS
      - os: macos-latest
      - node: 8

Another valid example:

runs-on: ${{ matrix.os }}
strategy:
  matrix:
    jvm: [8, 11]
    scala: [2.12.12, 2.13.5, 3.0.0]
    exclude:
      - jvm: 8
      - scala: 2.12.12

A last one:

runs-on: ${{ matrix.os }}
strategy:
  matrix:
    ruby: [2.7.3, 3.0.0]

(See: https://docs.github.com/en/actions/reference/workflow-syntax-for-github-actions#example-excluding-configurations-from-a-matrix)

For matrix in particular, we have multiple fields that are List Text, but we also have exclude that I believe is a List of Record.

I can write this code in Dhall if I'm just writing it from scratch, without defining types (and it seems to generate a Record with the specific keys I have.

However if I want to build a library with types, or more specifically extends this one, I can't figure out how to write the correct type. Typically, see this definition:

{ matrix : List { mapKey : Text, mapValue : List Text }
, fail-fast : Optional Bool
, max-parallel : Optional Natural
}

https://github.com/regadas/github-actions-dhall/blob/master/types/Strategy.dhall

matrix is defined as a List { mapKey : Text, mapValue : List Text }, but exclude is not a List Text so it doesn't work. And I can't figure out how to change this definition to accept exclude.

Note that in the example it was os and node, but it can be any key, and any number of key.

So any idea how to define that type?

Edit: added more examples

Answer 1

It looks this requires a change to the upstream github-actions-dhall repository. Specifically, matrix should probably be a record of Optional fields rather than a Map. It would probably have at least these fields based on your example:

{ os : Optional (List Text)
, node : Optional (List Natural)
, exclude : { os : Optional Text, node : Optional Natural }
}

For more guidance, see these chapters of the Dhall manual, which talk about how to model Dhall types when binding to configuration formats:

• How to convert an existing YAML configuration file to Dhall
• How to support default values

Edit: An easy way to convert example YAML configurations to either a Dhall value or the corresponding Dhall type is to use yaml-to-dhall. For example, if you take the three examples you gave me and stick them in a YAML array (one element per example), like this:

- runs-on: ${{ matrix.os }}
  strategy:
    matrix:
      os: [macos-latest, windows-latest, ubuntu-18.04]
      node: [8, 10, 12, 14]
      exclude:
        # excludes node 8 on macOS
        - os: macos-latest
        - node: 8
- runs-on: ${{ matrix.os }}
  strategy:
    matrix:
      jvm: [8, 11]
      scala: [2.12.12, 2.13.5, 3.0.0]
      exclude:
        - jvm: 8
        - scala: 2.12.12
- runs-on: ${{ matrix.os }}
  strategy:
    matrix:
      ruby: [2.7.3, 3.0.0]

Then you can ask yaml-to-dhall what type you can use that unifies all three of those examples, like this:

$ yaml-to-dhall type < examples.yaml  
List
  { runs-on : Text
  , strategy :
      { matrix :
          { exclude :
              Optional
                ( List
                    { jvm : Optional Natural
                    , node : Optional Natural
                    , os : Optional Text
                    , scala : Optional Text
                    }
                )
          , jvm : Optional (List Natural)
          , node : Optional (List Natural)
          , os : Optional (List Text)
          , ruby : Optional (List Text)
          , scala : Optional (List Text)
          }
      }
  }

Then if you just remove the List from the inferred type, then that is a valid type for your configuration that can handle those three examples:

  { runs-on : Text
  , strategy :
      { matrix :
          { exclude :
              Optional
                ( List
                    { jvm : Optional Natural
                    , node : Optional Natural
                    , os : Optional Text
                    , scala : Optional Text
                    }
                )
          , jvm : Optional (List Natural)
          , node : Optional (List Natural)
          , os : Optional (List Text)
          , ruby : Optional (List Text)
          , scala : Optional (List Text)
          }
      }
  }

… and yaml-to-dhall can also show you what the corresponding Dhall values of that type would be:

$ ✓ yaml-to-dhall < examples.yaml     
[ { runs-on = "\${{ matrix.os }}"
  , strategy.matrix
    =
    { exclude = Some
      [ { jvm = None Natural
        , node = None Natural
        , os = Some "macos-latest"
        , scala = None Text
        }
      , { jvm = None Natural, node = Some 8, os = None Text, scala = None Text }
      ]
    , jvm = None (List Natural)
    , node = Some [ 8, 10, 12, 14 ]
    , os = Some [ "macos-latest", "windows-latest", "ubuntu-18.04" ]
    , ruby = None (List Text)
    , scala = None (List Text)
    }
  }
, { runs-on = "\${{ matrix.os }}"
  , strategy.matrix
    =
    { exclude = Some
      [ { jvm = Some 8, node = None Natural, os = None Text, scala = None Text }
      , { jvm = None Natural
        , node = None Natural
        , os = None Text
        , scala = Some "2.12.12"
        }
      ]
    , jvm = Some [ 8, 11 ]
    , node = None (List Natural)
    , os = None (List Text)
    , ruby = None (List Text)
    , scala = Some [ "2.12.12", "2.13.5", "3.0.0" ]
    }
  }
, { runs-on = "\${{ matrix.os }}"
  , strategy.matrix
    =
    { exclude =
        None
          ( List
              { jvm : Optional Natural
              , node : Optional Natural
              , os : Optional Text
              , scala : Optional Text
              }
          )
    , jvm = None (List Natural)
    , node = None (List Natural)
    , os = None (List Text)
    , ruby = Some [ "2.7.3", "3.0.0" ]
    , scala = None (List Text)
    }
  }
]

… although you will probably want to shorten that using Dhall's support for schemas. The above link to the Dhall manual on default handling has more details, but the short summary is that you can save the following three schemas to a file named ./schemas.dhall:

-- ./schemas.dhall

let Exclusion =
      { Type =
          { jvm : Optional Natural
          , node : Optional Natural
          , os : Optional Text
          , scala : Optional Text
          }
      , default =
        { jvm = None Natural
        , node = None Natural
        , os = None Natural
        , scala = None Text
        }
      }

let Matrix =
      { Type =
          { exclude : Optional (List Exclusion.Type)
          , jvm : Optional (List Natural)
          , node : Optional (List Natural)
          , os : Optional (List Text)
          , ruby : Optional (List Text)
          , scala : Optional (List Text)
          }
      , default =
        { exclude = None (List Exclusion.Type)
        , jvm = None (List Natural)
        , node = None (List Natural)
        , os = None (List Text)
        , ruby = None (List Text)
        , scala = None (List Text)
        }
      }

let Config =
      { Type = { runs-on : Text, strategy : { matrix : Matrix.Type } }
      , default = {=}
      }

in  { Exclusion, Matrix, Config }

… and then rewrite the result to use those schemas, like this:

$ yaml-to-dhall < examples.yaml | dhall rewrite-with-schemas --schemas ./schemas.dhall
let schemas = ./schemas.dhall

in  [ schemas.Config::{
      , runs-on = "\${{ matrix.os }}"
      , strategy.matrix
        = schemas.Matrix::{
        , exclude = Some
          [ schemas.Exclusion::{ os = Some "macos-latest" }
          , schemas.Exclusion::{ node = Some 8, os = None Text }
          ]
        , node = Some [ 8, 10, 12, 14 ]
        , os = Some [ "macos-latest", "windows-latest", "ubuntu-18.04" ]
        }
      }
    , schemas.Config::{
      , runs-on = "\${{ matrix.os }}"
      , strategy.matrix
        = schemas.Matrix::{
        , exclude = Some
          [ schemas.Exclusion::{ jvm = Some 8, os = None Text }
          , schemas.Exclusion::{ os = None Text, scala = Some "2.12.12" }
          ]
        , jvm = Some [ 8, 11 ]
        , scala = Some [ "2.12.12", "2.13.5", "3.0.0" ]
        }
      }
    , schemas.Config::{
      , runs-on = "\${{ matrix.os }}"
      , strategy.matrix = schemas.Matrix::{ ruby = Some [ "2.7.3", "3.0.0" ] }
      }
    ]