Newbie here: Having trouble with nested default values and partial records

#1

Hi there. Trying to produce TOML like the following:

[plugins.pure]
github = "sindresorhus/pure"
use = "pure.zsh"

[plugins.zsh-async]
github = "mafredri/zsh-async"

At the moment, I’m running into issues with something like this:

let Plugin =
      { Type =
          { mapKey : Text
          , mapValue : { github : Optional Text, use : Optional (List Text) }
          }
      , default =
        { mapKey = "UNKNOWN", mapValue = { github = None Text, use = None (List Text)  } }
      }

let github-named =
      \(name : Text) ->
      \(slug : Text) ->
        { mapKey = name, mapValue.github = slug }

let github =
      \(user : Text) -> \(repo : Text) -> github-named repo "${user}/${repo}"

let plugins =
      [ github "mafredri" "zsh-async"
      , github "sindresorhus" "pure" // Plugin::{ mapValue.use = Some [ "pure.zsh" ]}
      , github "zsh-users" "zsh-autosuggestions"
      ]

I’m getting this error:

Error: Expression doesn't match annotation

{ mapValue : { - github : …
             , …
             }
, …
}

31│                                         Plugin::{ mapValue.use = Some [ "pure.zsh" ]}

Dotfiles/config/sheldon/plugins.dhall:31:41

I’m struggling to understand how to use record-defaults and right-combination to overwrite deeply nested fields of a record produced by a function. Halp? :weary:

#2

There is not a way to override a value within a Map. It is definitely not possible.

The way I would suggest doing this is the “two types” approach, which is that you have one type that users use for authoring the Dhall configuration, and then a second type that is used as the input to dhall-toml and a conversion function (e.g. render) that converts from the former type to the latter type.

The reason I suggest splitting your approach into two separate types is because it gets much easier to enforce correctness if you don’t include the repository name in the Plugin type that the user authors (since it’s already present in the Map key). In other words, removing the repository name from the Plugin type makes an invalid state unrepresentable by making it impossible for the two occurrences of the repository name to drift.

However, you still need the repository name to appear in the Plugin for the final TOML configuration, which is what the second type and the render function are for. It would look something like this:

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

let Config = Prelude.Map.Type Text

let Plugin =
      { Input =
        { Type = { name : Optional Text, use : Optional (List Text) }
        , default = { name = None Text, use = None (List Text) }
        }
      , Output =
        { Type = { github : Optional Text, use : Optional (List Text) }
        , default = { github = None Text, use = None (List Text) }
        }
      }

let -- The difference before and after is that before the `github` field doesn't
    -- include the repository name and after it does
    render
    : Config Plugin.Input.Type → Config Plugin.Output.Type
    = Prelude.List.map
        { mapKey : Text, mapValue : Plugin.Input.Type }
        { mapKey : Text, mapValue : Plugin.Output.Type }
        ( λ(entry : { mapKey : Text, mapValue : Plugin.Input.Type }) →
            { mapKey = entry.mapKey
            , mapValue = Plugin.Output::{
              , github =
                  Prelude.Optional.map
                    Text
                    Text
                    (λ(name : Text) → "${name}/${entry.mapKey}")
                    entry.mapValue.name
              , use = entry.mapValue.use
              }
            }
        )

let input
    : Config Plugin.Input.Type
    = toMap
        { zsh-async = Plugin.Input::{ name = Some "mafredri" }
        , pure = Plugin.Input::{
          , name = Some "sindresorhus"
          , use = Some [ "pure.zsh" ]
          }
        , zsh-autosuggestions = Plugin.Input::{ name = Some "zsh-users" }
        }

let plugins
    : Config Plugin.Output.Type
    = render input

in  { plugins }

… which produces this output:

{ plugins =
  [ { mapKey = "pure"
    , mapValue =
      { github = Some "sindresorhus/pure", use = Some [ "pure.zsh" ] }
    }
  , { mapKey = "zsh-async"
    , mapValue = { github = Some "mafredri/zsh-async", use = None (List Text) }
    }
  , { mapKey = "zsh-autosuggestions"
    , mapValue =
      { github = Some "zsh-users/zsh-autosuggestions", use = None (List Text) }
    }
  ]
}