Existential types explained in Idris code

Existential.idr

module Existential

%access public export

StackInterface : Type -> Type
StackInterface a = ( a
                   , Integer -> a -> a
                   , a -> (a, Integer)
                   )

Existential : (Type -> Type) -> Type
Existential phi = {b: Type} -> ({a: Type} -> phi a -> b) -> b

AbstractStack : Type
AbstractStack = Existential StackInterface

compute : AbstractStack -> Integer
compute stack = stack x
  where
    x : {a: Type} -> StackInterface a -> Integer
    x (empty, push, pop) =
      let (stk, v) = pop (push 12 $ push 5 empty)
          (stk2, v2) = pop stk
      in v + v2

listPush : a -> List a -> List a
listPush i l = i::l

listPop : List a -> (List a, a)
listPop (i::l) = (l, i)

listEmpty : List a
listEmpty = []

stack : AbstractStack
stack = (\t => t (listEmpty, listPush, listPop))

clistPush : a -> (List a, Integer) -> (List a, Integer)
clistPush i (l, n) = (i::l, n + 1)

clistPop : (List a, Integer) -> ((List a, Integer), a)
clistPop (i::l, n) = ((l, n - 1), i)

clistEmpty : (List a, Integer)
clistEmpty = (Nil, 0)

stack2 : AbstractStack
stack2 = (\t => t (clistEmpty, clistPush, clistPop))

twoStacks : List AbstractStack
twoStacks = [stack, stack2]

main : IO ()
main = print [compute currentStack | currentStack <- twoStacks]