Lisp apply in idris

Apply.idr

module Apply2

||| Heterogenious lists.
|||
|||```idris example
|||
||| hl : Hlist [Nat, (Double, Char), 1 = 1]
||| hl = [1, (3.0, 'a'), Refl]
|||```
data Hlist : List Type -> Type where
  ||| The empty Hlist
  Nil   : Hlist []
  ||| Add an element to an Hlist, keeping track of the type at its
  ||| position.
  |||
  ||| @ l the list of previous types
  ||| @ t the element
  |||
  ||| ```idris example
  |||
  ||| hl : Hlist [Int, String]
  ||| hl = 4 :: "example" :: []
  ||| ```
  (::)  : t -> Hlist l -> Hlist (t :: l)

||| Calculate a function type.
||| @ params in order
||| @ return fully evaluated type
|||
|||```idris example
|||
||| exf : Int -> String -> Bool -> String
||| exf i s b = if b then s else show i
|||
||| exg : [Int, String, Bool] `To` String
||| exg i s b = if b then s else show i
|||
||| to1 : (i : Int) -> (s : String) -> (b : Bool) -> Apply2.exf i s b = Apply2.exg i s b
||| to1 i s b = Refl
||| ```
To : (params : List Type) -> (return : Type) -> Type
To []        r = r
To (a :: as) r = a -> (as `To` r)

||| Apply a variadic function to some parameters.
||| @ return the type returned
||| @ params a list of types the function acceps
||| @ f the function
|||
||| ```idris example
|||
||| ex1 : apply' Basics.id [2] = 2
||| ex1 = Refl
|||
||| ex2 : apply' (+) [1000, -1] = 999
||| ex2 = Refl
|||
||| ex3 : apply' Foldable.foldr
|||       [Nat.mult, 1, the (List Nat) [3, 2, 10]]
|||      = 60
||| ex3 = Refl
||| ```
apply' : (f : To params return) -> Hlist params -> return
apply' x []        = x
apply' f (x :: xs) = apply' (f x) xs

---- Examples ----

||| Simple function accepting multiple values.
exf : Int -> String -> Bool -> String
exf i s b = if b then s else show i

||| Simple function accepting multiple values; whose type is
||| calculated using **To**
exg : [Int, String, Bool] `To` String
exg i s b = if b then s else show i

||| Example equality between a normal function and one calculated with
||| **To**.
to1 : (i : Int) -> (s : String) -> (b : Bool)
    -> Apply2.exf i s b = Apply2.exg i s b
to1 i s b = Refl

||| Example heterogeneous list
hl1 : Hlist [Int, String, Bool]
hl1 = [4, "hi", False]

||| Example of apply'.
ex1 : apply' (+) [1000, -1] = 999
ex1 = Refl

||| Example of apply'.
|||
||| Note module prefixes (Apply2.). Required since lowercase names
||| denote type variables.
ex2 : apply' Apply2.exf Apply2.hl1 = "4"
ex2 = Refl

||| Example of apply'.
|||
||| Note module prefixes (Basics.). Required since lowercase names
||| denote type variables.
ex3 : apply' Basics.id [2] = 2
ex3 = Refl

||| More complicated example of apply'.
|||
||| Note module prefixes (Foldable.). Required since lowercase names
||| denote type variables.
ex4 : apply' Foldable.foldr
      [Nat.mult, 1, the (List Nat) [3, 2, 10]]
     = 60
ex4 = Refl

||| More complicated example of apply'.
|||
||| Note module prefixes (Foldable.). Required since lowercase names
||| denote type variables.
ex5 : apply' (Foldable.foldr Nat.mult 1)
      [the (List Nat) [2, 4, 5, 5, 6]]
      = 1200
ex5 = Refl

||| Example of apply' creating a new function
ex6 : List Nat -> Nat
ex6 = apply' (foldr Nat.mult) [1]

||| Example of apply' creating a new function
ex7 : Hlist [Nat -> Nat -> Nat, Nat, List Nat] -> Nat
ex7 = apply' foldr

||| Example of apply' creating a new function
ex8 : Hlist [a -> b -> c, List a, List b] -> List c
ex8 = apply' zipWith