How to type-check and normalize incomplete code

Benefit from the language even when prototyping

You can type-check and normalize incomplete code by introducing a function argument named TODO that has the following type:

λ(TODO : ∀(a : Type) → a) → …

Then you can use TODO to fill any gaps in your code that have not been implemented yet:

  λ(TODO : ∀(a : Type) → a)
→ let List/map =
        https://prelude.dhall-lang.org/List/map

  let Text/concatSep =
        https://prelude.dhall-lang.org/Text/concatSep

  let Person = { name : Text, age : Natural }

  --  ↓ You can leave functions unimplemented
  let renderPerson = TODO (Person → Text)

  let renderList =
        λ(elements : List Text) → "[" ++ Text/concatSep ", " elements ++ "]"

  let renderPeople
      : List Person → Text
      =   λ(people : List Person)
        → renderList (List/map Person Text renderPerson people)

  in  renderPeople
      [ { name = "John", age = 23 }
      , TODO Person  -- ← You can also leave values unimplemented
      , { name = "Mary", age = 24 }
      ]

The type ∀(a : Type) a is an impossible type that can never be created in Dhall, so the TODO function argument can never be satisfied. However, despite that we can still type-check the function and normalize the function body:

$ dhall --annotate <<< './example.dhall'
  (   λ(TODO : ∀(a : Type) → a)
    →     "["
      ++  (     TODO
                ({ age : Natural, name : Text } → Text)
                { age = 23, name = "John" }
            ++  ", "
            ++  TODO
                ({ age : Natural, name : Text } → Text)
                (TODO { age : Natural, name : Text })
            ++  ", "
            ++  TODO
                ({ age : Natural, name : Text } → Text)
                { age = 24, name = "Mary" }
          )
      ++  "]"
  )
: ∀(TODO : ∀(a : Type) → a) → Text