Dhall的渐进式打字

Question

Dhall网站有一个很好的例子：

{- You can optionally add types

   `x : T` means that `x` has type `T`
-}

let Config : Type =
      {- What happens if you add another field here? -}
      { home : Text
      , privateKey : Text
      , publicKey : Text
      }

let makeUser : Text -> Config = \(user : Text) ->
      let home       : Text   = "/home/${user}"
      let privateKey : Text   = "${home}/.ssh/id_ed25519"
      let publicKey  : Text   = "${privateKey}.pub"
      let config     : Config = { home, privateKey, publicKey }
      in  config

let configs : List Config =
      [ makeUser "bill"
      , makeUser "jane"
      ]

in  configs

就像注释要求我做的那样，我添加了另一个字段：foo : Text到Config类型，而现在这个示例无法进行类型检查。这使我无法逐步向现有项目添加类型。我错过了一个逃生舱口，让我可以逐渐增加知识，因为我变得更加熟悉的动态配置的项目，我不拥有。

我敢打赌，这是一种常见的情况：“我正在维护一个我不拥有的项目，在YAML或JSON中配置，没有模式，或者使用一个松散定义的模式。”

我相信我想要的是所谓的“行多态”，好像已经讨论过了 (并拒绝了？)在Dhall问题上，我有什么办法可以解决同样的问题呢？从我的角度来看，在我没有全部信息的情况下，我似乎不能使用Dhall？

Answer 1

您说得对，最符合人体工程学的解决方案将是对行多态性的语言支持。例如，请参阅另一个支持行多态性的概念证明项目：

• 失宠

然而，Dhall确实有一个语言特性，它在这里仍然有帮助，这就是支持按预期类型投影记录的字段。换句话说，如果一个记录r包含Config中字段的超集，那么您就可以使用r.(Config)来投影感兴趣的字段。

通常，我会在您从dhol-lang.org引用的示例的上下文中说明这是如何工作的，但这个特定示例的问题是，它不可能默默地忽略额外foo字段的存在，即使Dhall支持行多态性。这是因为makeUser函数生成一个Config而不是使用一个Config，所以如果您承诺生成额外的字段，那么您必须实际添加预期的字段。

然而，本着您的请求精神，我将使用一个相关的例子，我认为这更接近您的想法。唯一的区别是，我们将把函数更改为消耗Config的函数

let Config : Type = { home : Text, privateKey : Text, publicKey : Text }

let render =
      λ(config : Config) →
        ''
        Home: ${config.home}
        Private Key: ${config.privateKey}
        Public Key: ${config.publicKey}
        ''

let example =
      { home = "/home/gabriella"
      , privateKey = "/home/gabriella/.ssh/id_ed25519"
      , publicKey = "/home/gabriella/.ssh/id_ed25519.pub"
      }

in  render example

我们希望能够在示例中添加另一个foo字段，但不破坏render函数。换句话说，我们希望render函数无声地忽略Config类型中的字段以外的任何字段。

通常，在具有行多态性的语言中，您可以通过将render的类型更改为如下所示来解决这个问题：

let render =
      λ(config : { home : Text, privateKey : Text, privateKey : Text | r }) →
        ''
        Home: ${config.home}
        Private Key: ${config.privateKey}
        Public Key: ${config.publicKey}
        ''

let example =
      { home = "/home/gabriella"
      , privateKey = "/home/gabriella/.ssh/id_ed25519"
      , publicKey = "/home/gabriella/.ssh/id_ed25519.pub"
      , foo = "bar"
      }

in  render example

…其中，r在render类型中表示“我们希望忽略的其他字段”。正如您所指出的，Dhall不支持这种方法，但是如果我们使用Dhall对按类型投影字段的支持，我们可以这样做：

let Config : Type = { home : Text, privateKey : Text, publicKey : Text }

let render =
      λ(config : Config) →
        ''
        Home: ${config.home}
        Private Key: ${config.privateKey}
        Public Key: ${config.publicKey}
        ''

let example =
      { home = "/home/gabriella"
      , privateKey = "/home/gabriella/.ssh/id_ed25519"
      , publicKey = "/home/gabriella/.ssh/id_ed25519.pub"
      , foo = "bar"
      }

in  render example.(Config)

它不像行多态那样符合人体工程学，但至少它解决了代码对添加新字段的上游输入中的更改不敏感的用例。