dhall - 为什么 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 表达式，dhall-haskell也是如此，感谢@gabriel-gonzales

Answer 1

由于它是如何演变的，这是语言中无意的不一致，并且可以修复不一致。

当该语言首次发布时，既if不能也merge不能返回类型。后来，联合和merge更新以允许此拉取请求中的类型：

• 允许记录字段和联合选项成为类型

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