Fun with Boehm-Berarduccin encoding, in Dhall, where you really need it

bbencoding.dhall

-- https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html

let Person : Type
  = ∀(Person : Type)
  → ∀(MakePerson : { children : List Person, name : Text } → Person)
  → Person

let example : Person
  = λ(Person : Type) →
    λ(MakePerson : { children : List Person, name : Text } → Person) →
    MakePerson
      { children =
          [ MakePerson { children = [] : List Person, name = "Sally" }
          , MakePerson { children = [] : List Person, name = "Bobby" }
          ]
      , name = "друг"
      }

let everybody : Person → List Text
  = let concat = http://prelude.dhall-lang.org/List/concat
    in λ(p : Person) →
         p (List Text)
           ( λ(p : { children : List (List Text), name : Text }) →
               [ p.name ] # concat Text p.children
           )

in everybody example

bbencodingrec.dhall

-- https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html

let Nat : Type
  = ∀(Nat : Type)
  → ∀(Zero : Nat)
  → ∀(Succ : Nat -> Nat)
  → Nat

let three : Nat
  = λ(Nat : Type) →
    λ(Zero : Nat) →
    λ(Succ : Nat -> Nat) →
      Succ (Succ (Succ Zero))

let toNatural : Nat → Natural
  = λ(n : Nat) -> n Natural 0 (λ(m : Natural) → 1 + m)

in toNatural three

bbencodingrec2.dhall

-- https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html

let Tree : (Type -> Type)
  = λ(Elem : Type)
  → ∀(Tree : Type)
  → ∀(MakeNode : { value : Elem, left : Tree, right : Tree } → Tree)
  → ∀(Leaf : Tree)
  → Tree

let example : Tree Natural
  = λ(Tree : Type) →
    λ(MakeNode : { value : Natural, left : Tree, right : Tree } → Tree) →
    λ(Leaf : Tree) →
    MakeNode
      { value = 3
      , left = MakeNode
                 { value = 1
                 , left = Leaf
                 , right = Leaf
                 }
      , right = MakeNode
                  { value = 2
                  , left = Leaf
                  , right = Leaf
                  }
      }

let preorder : ∀(Elem : Type) → Tree Elem -> List Elem
  = λ(Elem : Type) →
    λ(t : Tree Elem) →
    t (List Elem)
      ( λ(t : { value : Elem, left : List Elem, right: List Elem }) →
          [ t.value ] # t.left # t.right
      )
      ([] : List Elem)

in preorder Natural example