4

我正在尝试在 Dhall 中定义多态类型。在 Haskell 中，它看起来像：

data MyType a = Some a | SomethingElse

为此，我在 Dhall (mkMyType.dhall) 中定义了这个函数：

let SomethingElse = ./SomethingElse.dhall  in λ(a : Type) → < some : a | somethingElse : SomethingElse >

我还定义了一个函数，它返回该类型的构造函数，给定一个 (./mkMyTypeConstructor.dhall)：

λ(a : Type) → constructors (./mkMyType.dhall a)

现在，为了使用它，我需要执行以下操作：

(./mkMyTypeConstructor.dhall Text).some "foo"

这是正确的方法吗？

最后，在我的用例中最理想的类型是对诸如“foo”之类的文本和自定义类型（例如 { somethingElse: {} }）进行类型检查。这可能吗？

4

1 回答 1

4

我将使用类似于 Haskell 的联合类型Either来保持以下示例自包含。

假设我们保存以下Either.dhall文件：

-- Either.dhall
λ(a : Type) → λ(b : Type) → < Left : a | Right : b >

我们*可以提供这样的makeEither.dhall文件：

-- makeEither.dhall
λ(a : Type) → λ(b : Type) → constructors (./Either.dhall a b)

...然后我们可以像这样使用该文件：

[ (./makeEither.dhall Text Natural).Left "Foo"
, (./makeEither.dhall Text Natural).Right 1
]

...但这不符合人体工程学。

例如，./makeEither.dhall Text Natural不需要重复写入，因为我们可以使用let表达式来减少重复，如下所示：

    let either = ./makeEither.dhall Text Natural

in  [ either.Left "Foo", either.Right 1 ]

另外，请注意，我们可以使用constructors和Either.dhall直接在大约相同数量的空间中：

    let either = constructors (./Either.dhall Text Natural)

in  [ either.Left "Foo", either.Right 1 ]

...这意味着我们不再需要中间makeEither.dhall文件了。

最后一个例子是我推荐的方法。具体来说：

  • 使用let表达式避免重复使用constructors关键字
  • 让最终用户自己打电话constructors而不是替他们打电话

对于你的后一个问题，我认为这应该放在一个单独的 StackOverflow 问题中。

编辑：请注意，constructors关键字现在已过时，您现在可以只写：

let either = ./Either.dhall Text Natural

in  [ either.Left "Foo", either.Right 1 ]

有关更多详细信息，请参阅：

于 2018-07-31T20:51:15.240 回答