How to make a recursive Dhall sum type containing data

Question

Here is my example code. I haven't been able to figure out how to make my State sum-type recursive, while still allowing it to be used like a sum-type elsewhere. Likewise with my StateMachine type.

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

Is there a reasonable way to do this that doesn't blow up code size and make the types ergonomic for an end user to import and use? In case it wasn't apparent from the example, I'm trying to mode a state machine.

I have tried the following, but I get a "Not a record or a Union" error for State.Task:

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

Answer 1

First, I believe the type you meant to say was:

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

in  State

To answer your question, the closest thing you can get to a recursive union type is this equivalent representation:

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

in  State

... but you wouldn't get union constructors for free so I wouldn't recommend using the latter representation anyway.

For either approach you'd have to create functions that behave the same way as constructors; the language won't generate them for you like it does for non-recursive union types.

I'll illustrate how to write the constructors for the first type since that's the representation I'd recommend using:

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 }
      }

For more details, see:

• How to translate recursive code to Dhall