如何在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：{} )输入check。这个是可能的吗？

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 ]

另外，请注意，我们可以在大约相同的空间中直接使用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 ]

有关更多细节，请参见：

• keyword