-- ifNil and ifNode derived from data constructors. I call them "ops",
-- package them in a record type.
let Ops
    : Type -> Type
    = \(r : Type) -> { ifNil : r, ifNode : Integer -> r -> r }

let InvListZ
    : Type
    = forall (r : Type) -> Ops r -> r

let example =
      \(r : Type) ->
      \(op : Ops r) ->
        op.ifNode +4 (op.ifNode +1 (op.ifNode +6 op.ifNil))

let Integer/add = https://prelude.dhall-lang.org/Integer/add

let mySum
    : InvListZ -> Integer
    = \(xs : InvListZ) -> xs Integer { ifNil = +0, ifNode = Integer/add }

let toInvListZ
    : List Integer -> InvListZ
    = \(xs : List Integer) ->
      \(r : Type) ->
      \(op : Ops r) ->
        List/fold Integer xs r op.ifNode op.ifNil
        -- Dhall List/fold is foldr but different argument order.

let fromInvListZ
    : InvListZ -> List Integer
    = \(xs : InvListZ) ->
        xs
          (List Integer)
          { ifNil = [] : List Integer
          , ifNode = \(x : Integer) -> \(xs : List Integer) -> [ x ] # xs
          }

in  mySum example