Skip to content

Functions

Functions as arguments

Functions are higher-order → pass as arguments or return as results, etc.

Basic example

1
2
3
4
5
6
7
8
9
(* define basic function *)
Definition add_self (n:nat):= n + n.

(* function with function argument *)
Definition do_3_times {X:Type} (f:X -> X) (n:X) : X :=
  f (f (f n)).

(* call them *)
Compute do_3_times add_self 1.

More interesting examples

Filter and map list elements

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
(* return list items for which test is true *)
Fixpoint filter {X:Type} (test: X -> bool) (l:list X) : (list X) :=
  match l with
  | [] => []
  | h :: t =>
    if test h then h :: (filter test t)
    else filter test t
end.

(* apply f to each list element
   note: X and Y can be different types *)
Fixpoint map {X Y: Type} (f:X -> Y) (l:list X) : (list Y) :=
match l with
  | [] => []
  | h :: t => (f h) :: (map f t)
end.

Fold inserts a binary operator between list elements

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
Fixpoint fold {X Y: Type} (f: X->Y->Y) (l: list X) (b: Y) : Y :=
match l with
  | nil => b
  | h :: t => f h (fold f t b)
end.

(* use it *)
Compute fold plus [1,2,3,4] 0.  (* = 10 *)`} />

## Returning a function

```coq
(* define function that returns a function *)
Definition constfun {X: Type} (x: X) : nat -> X :=
  (* very silly function *)
  fun (k:nat) => x.

Compute (constfun true) 0. (* true *)
Compute (constfun 5) 99.     (* 5 *)

Anonymous functions

  • use fun to create anonymous function for one-time use
1
Compute do_3_times (fun n => n * n) 2.