在 dhall 中定义复杂类型的列表

Question

我定义了几种类型，其中两种被组织成列表（字段和选项）。定义函数以帮助定义条目（addfield 和 addoption）。我能够定义字段并按预期工作；但是，对于选项，当列表包含多个元素时，我会收到错误消息。

这是完整的 dhall 文件：

let FTypes = < U8 | U16 | U32 | F32 | BITS >

let Translate = List { mapKey : Text, mapValue : Text }

let Bits = < Bit0 | Bit1 | Bit2 | Bit3 | Bit4 | Bit5 | Bit6 | Bit7 >

let bits2Natural
    : Bits → Natural
    = λ(b : Bits) →
        merge
          { Bit0 = 0
          , Bit1 = 1
          , Bit2 = 2
          , Bit3 = 3
          , Bit4 = 4
          , Bit5 = 5
          , Bit6 = 6
          , Bit7 = 7
          }
          b

let Field =
      let TypeBits = { bit : Natural, width : Natural }
      in  { Type =
              { startbyte : Natural
              , type : FTypes
              , translate : Optional Translate
              , typebits : Optional TypeBits
              }
          , default = { translate = None Translate, typebits = None TypeBits }
          }

let FieldList = List { mapKey : Text, mapValue : Field.Type }

let Option = { dlc : Natural, fields : FieldList, telemjson : Optional Text }

let OptionList = List { mapKey : Text, mapValue : Option }

let addfield = λ(n : Text) → λ(f : Field.Type) → { mapKey = n, mapValue = f }

let addoption = λ(k : Text) → λ(v : Option) → { mapKey = k, mapValue = v }

let testoption : OptionList =
    [ addoption "0"
        { dlc = 4
        , fields =
            [ addfield "field0" Field::{startbyte = 1, type = FTypes.U16 }
            , addfield "field1" Field::{startbyte = 3, type = FTypes.U8 }
            ]
        , telemjson = Some 
            (  "{\"sensor1\":{"
            ++ "\"time\":\"@(timestamp)\","
            ++ "\"id\":\"@(option)\","
            ++ "\"temp\":@(field0.value),"
            ++ "\"unit\":\"@(field1.value)\""
            ++ "}}"
            )
        }
    , addoption "1"
        { dlc = 2
        , fields = [ addfield "field0" Field::{startbyte = 1, type FTypes.U8 } ]
        , telemjson = Some
            ("{\"sensor2\":{\"value\":@(field1.value)}}")
        }
    ]
    
in testoption

这是错误输出：

Error: Invalid input

trial2.dhall:60:9:
   |
60 |         { dlc = 2
   |         ^
unexpected '{'
expecting ',', ->, :, ], or whitespace

如果我删除第二个选项（第 59-64 行），它会起作用吗？

我做错了什么？如何为 OptionList.

定义多个 Option

Answer 1

解析错误可以改进，但由于此处缺少 = 符号，从第 60 行开始的记录中存在拼写错误：

        , fields = [ addfield "field0" Field::{startbyte = 1, type FTypes.U8 } ]
                                                                  ↑

应该是：

        , fields = [ addfield "field0" Field::{startbyte = 1, type = FTypes.U8 } ]

... 如果您进行了更改，则文件会成功解析并且 type-checks.

在 dhall 中定义复杂类型的列表

Defining a list of complex Type in dhall

dhall