如何制作包含数据的递归 Dhall 和类型

Question

这是我的示例代码。我一直无法弄清楚如何使我的 State 求和类型递归，同时仍然允许它像其他地方的求和类型一样使用。我的 StateMachine 类型也是如此。

let State =
      < Task : { Comment : Text, Resource : Text, End : Bool }
      | Map : { Comment : Text, Iterator : StateMachine }
      | Parallel : { Comment : Text, Branch : List State }
      >

let StateMachine
    : Type
    = { Comment : Optional Text
      , StartAt : Text
      , States : List { mapKey : Text, mapValue : State }
      }

let test
    : StateMachine
    = { Comment = Some "A simple minimal example"
      , StartAt = "Hello World"
      , States =
        [ { mapKey = "Hello World"
          , mapValue =
              State.Task { Type = "Task", Resource = "Test", End = True }
          }
        ]
      }

in  test

有没有一种合理的方法可以做到这一点，既不会增加代码大小，又能使最终用户导入和使用的类型符合人体工程学？如果从示例中看不出来，我正在尝试对状态机进行模式设置。

我尝试了以下方法，但是 State.Task 出现 "Not a record or a Union" 错误：

let State
    : Type
    =   ∀(_State : Type)
      → ∀(Task : { Type : Text, Resource : Text, End : Bool })
      → ∀(Map : { Type : Text, Iterator : _State })
      → _Stat

Answer 1

首先，我认为您要说的类型是：

let State
    : Type
    = ∀(State : Type) →
      ∀(Task : { Type : Text, Resource : Text, End : Bool } → State) →
      ∀(Map : { Type : Text, Iterator : State } → State) →
        State

in  State

为了回答您的问题，最接近递归联合类型的是以下等效表示：

let State
    : Type
    = ∀(State : Type) →
      ( < Task : { Type : Text, Resource : Text, End : Bool }
        | Map : { Type : Text, Iterator : State }
        > →
          State
      ) →
        State

in  State

...但是您不会免费获得联合构造函数，因此无论如何我都不建议使用后一种表示形式。

对于任何一种方法，您都必须创建与构造函数行为相同的函数；该语言不会像为非递归联合类型那样为您生成它们。

我将说明如何为第一种类型编写构造函数，因为这是我推荐使用的表示形式：

let Types =
      let Task = { Type : Text, Resource : Text, End : Bool }

      let Map = λ(State : Type) → { Type : Text, Iterator : State }

      let State
          : Type
          = ∀(State : Type) →
            ∀(Task : Task → State) →
            ∀(Map : Map State → State) →
              State

      in  { Task, Map, State }

let -- Record of constructors similar to what you would get from a union type
    State =
      let Task
          : Types.Task → Types.State
          = λ(x : Types.Task) →
            λ(State : Type) →
            λ(Task : Types.Task → State) →
            λ(Map : Types.Map State → State) →
              Task x

      let Map
          : Types.Map Types.State → Types.State
          = λ(x : Types.Map Types.State) →
            λ(State : Type) →
            λ(Task : Types.Task → State) →
            λ(Map : Types.Map State → State) →
              Map (x with Iterator = x.Iterator State Task Map)

      in  { Task, Map }

in  State.Map
      { Type = "Foo"
      , Iterator = State.Task { Type = "Bar", Resource = "CPU", End = False }
      }

详情请见：

How to translate recursive code to Dhall

如何制作包含数据的递归 Dhall 和类型

How to make a recursive Dhall sum type containing data

dhall