Search code examples
dhall

Why doesn't Dhall allow returning types from if expressions?

Dhall has functions that return types:

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

And it has if expressions:

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

But the two features can't be used together:

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

in 3

Why?

At first I thought this was a trick to avoid having dependent types, but it seems Dhall does allow types to really depend on values when working with unions. The following compiles fine:

let MyBool = <T | F>

let myIf: MyBool -> Type = \(b: MyBool) ->
        merge
          { T = Bool
          , F = Natural
          }
          b
          
in 3

UPDATE

The dhall standard supports such if expressions now, as does dhall-haskell, thanks @gabriel-gonzales

Solution

  • It's an unintentional inconsistency in the language due to how it evolved, and the inconsistency can be fixed.

    When the language was first released neither if nor merge could return a type. Later on, unions and merge were updated to permit types in this pull request:

    … but we haven't yet updated if expressions with a matching change.