Dhall implementation of `take`

take.dhall

{- This is a bit ugly and inefficient.  See this thread for a discussion about
   adding a `Natural/subtract` built-in to improve this:

   https://github.com/dhall-lang/dhall-lang/issues/602#issuecomment-505484434
-}
let Natural/predecessor : Natural → Natural
        = λ(n : Natural)
        → let result = Natural/fold
          n
          (Optional Natural)
          (λ(o : Optional Natural) →
              Optional/fold Natural o (Optional Natural) (λ(m : Natural) → Some (m + 1)) (Some 0)
          )
          (None Natural)

          in Optional/fold Natural result Natural (λ(m : Natural) → m) 0

let Natural/subtract : Natural → Natural → Natural
        = λ(x : Natural)
        → λ(y : Natural)
        → Natural/fold x Natural Natural/predecessor y

let Natural/take : Natural → ∀(a : Type) → List a → List a
        = λ(n : Natural)
        → λ(a : Type)
        → λ(xs : List a)
        →     List/build
              a
              ( λ(list : Type)
              → λ(cons : a → list → list)
              → λ(nil : list)
              → List/fold
                { index : Natural, value : a }
                (List/indexed a xs)
                list
                ( λ(ix : { index : Natural, value : a })
                → λ(rest : list)
                →   if Natural/isZero (Natural/subtract n (ix.index + 1))
                    then cons ix.value rest
                    else rest
                )
                nil
              )

in  Natural/take