CODEWITHSUNDEEP
coq
Greg Nisbet
Greg Nisbet

Reputation: 6994

Coq polymorphic function without explicit type

I have an "enumerate" function written in the Coq term language (what is it called?). This function is kind of annoying to use because it requires that A (the type of an element in the list l) be explicitly provided whenever the enumerate function is used. Is there a way to avoid needing to explicitly pass A as a parameter?

(* [a, b] -> [(0,a), (1,b)] *)
Fixpoint enumerate (A : Type) (l : list A) : list (nat * A) :=
  let empty : (list (nat * A)) := nil in
  let incr_pair xy := match xy with 
   | (x, y) => ((S x), y)
  end in 
  match l with
  | nil => empty
  | (x :: xs) => (O, x) :: (map incr_pair (enumerate A xs))
  end.

I want to be able to write something like

Fixpoint enumerate (l : list A) : list (nat * A) := ...

Possibly with some additional syntax identifying what exactly A is.

Upvotes: 0

Views: 108

Answers (1)

András Kovács
András Kovács

Reputation: 30113

Put arguments in brackets to make them implicit by default (see section 2.7.4 here). Also, you should probably write this function in a non-quadratic way with a nat accumulator.

Require Import Lists.List.
Import ListNotations.

Fixpoint enumerate_from {A : Type} (n : nat) (l : list A) : list (nat * A) :=
  match l with
  | [] => []
  | x :: xs => (n, x) :: enumerate_from (S n) xs
  end.

Definition enumerate {A} l : list (nat * A) := enumerate_from 0 l.

Compute (enumerate [3; 4; 5]). (* prints [(0, 3); (1, 4); (2, 5)] *)

Upvotes: 3

Related Questions