如何在Dhall中编写处理Union类型的函数

Question

我正试图弄清楚Dhall中的编程是如何工作的。考虑以下联合类型：

let Object = < NoId | WithId : Text >

我想写一个函数extractId，它返回一个包含Id (或None)的Optional Text，但是我找不到一种在Dhall中进行解构的方法。

Answer 1

答案是使用merge函数。对于联合类型的每个构造函数，它都需要一个具有一个处理函数的集合。因此，要将上面的示例联合转换为Optional Text，我们可以这样做：

let someObject = Object.NoId

let handlers = { NoId = None Text, WithId = λ(t : Text) → Some t }

in  merge handlers someObject