为什么 Dhall 不允许从 if 表达式返回类型？

Question

Dhall具有返回类型的函数：

let f = (b : Bool) -> Natural                   -- ok

它有if表达式：

let f = (b: Bool) -> if b == True then 1 else 0 -- ok

但这两个功能不能同时使用：

-- Error: ❰if❱ branch is not a term 
let f= (b : Bool) -> if b == True then Natural else Integer
in 3

为什么？

起初，我认为这是一个避免依赖类型的技巧，但在与工会合作时，Dhall似乎确实允许类型真正依赖于价值观。以下编译良好：

let MyBool = <T | F>
let myIf: MyBool -> Type = (b: MyBool) ->
merge
{ T = Bool
, F = Natural
}
b

in 3

更新

dhall标准现在支持这样的if表达式，dhallhaskell也是如此，感谢@gabriel gonzales

Answer 1

由于语言的演变方式，这是一种无意的不一致，这种不一致可以修复。

当该语言首次发布时，if和merge都不能返回类型。稍后，union和merge被更新为允许此拉取请求中的类型：

• 允许记录字段和并集备选项为类型

…但我们还没有用匹配的更改更新if表达式。