haskell - 如何在 dhall 中使用多态类型构造函数

Question

我正在尝试在 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: {} })进行类型检查。这可能吗？

Answer 1

我将使用类似于 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 ]

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

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

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

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

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

• 使用 let 表达式以避免重复使用 constructors 关键字
• 让最终用户自己调用构造函数，而不是为他们调用

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

编辑:请注意，constructors 关键字现已过时，您现在只需编写:

let either = ./Either.dhall Text Natural

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

更多详情请参见:

• Migration: Deprecation of constructors keyword