Блог

У 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

Это непреднамеренное несоответствие в языке из-за того, как он развивался, и несоответствие может быть исправлено.

Когда язык был впервые выпущен if , ни merge один из них не мог возвращать тип. Позже объединения и merge были обновлены, чтобы разрешить типы в этом запросе на извлечение:

• Разрешить полям записи и альтернативам объединения быть типами

… но мы еще не обновили if выражения соответствующим изменением.