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

问题描述

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 standard和dhall-haskell一样现在都支持if表达式，感谢@ gabriel-gonzales

解决方法

由于语言的演变，这是一种无意间的不一致，可以解决这种不一致。

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

• Allow record fields and union alternatives to be types

…，但我们尚未更新if表达式，但有匹配的更改。