(** * INITIATION TO COQ: types as parameters, implicit arguments *)

(** We saw that types can be computed.  Types can also be used as
    parameters.  A common usage of this feature is to define
    *polymorphic* lists, that is, lists paramerized by the type of
    their elements, rather than defining lists of nats, lists of
    colors, etc., whereas many programs (length, concatenation,..)
    do not depend of elements.

    Here is a first definition of polymorphic lists of type [list A],
    where [A] is the type of the elements.

 *)

Inductive list (A : Set) : Set :=
| Nil : list A
| Cons : A -> list A -> list A.

(**
    The functional notation used for [list] means [list] can be seen
    as a function taking the type of elements in argument, and returning
    the corresponding type of lists.

    In contrast with previous functions such as [waow], no computation
    will be performed about types: [A] will be transfered as is to
    functions and constructors on lists.
*)


(** Let us see a concrete example, lists of natural numbers: we just
    take [nat] as an actual parameter of [list].
    Basically, it has to be repeated everywhere. *)
Example list624 : list nat := Cons nat 6 (Cons nat 2 (Cons nat 4 (Nil nat))).

(** This is quite heavy.  Moreover, [nat] can be guessed since it
    is the type of the elements.  We can write [_] as a placeholder
    of arguments that can be guessed. *)

Reset list624.
Example list624 := Cons _ 6 (Cons _ 2 (Cons _ 4 (Nil _))).

(** Better, but still somewhat heavy.
    And values are still displayed in a heavy manner. *)
Print list624.

(** A better alternative is to state that [A] is an *implicit*
    argument, as follows. *)

Reset list624.
Arguments Nil {A}.
Arguments Cons {A}.

Example list624 := Cons 6 (Cons 2 (Cons 4 Nil)).
Print list624.

(** However, implicit argument are only a presentation artifact:
    Coq keeps the full term in its internal representation. *)

Set Printing All.
Print list624.

(** Prefixing a name by [@] provides its explicit version. *)

Unset Printing All.
Print list624.

(** Version of the length where [A] is an ordinary explicit argument *)
Fixpoint length_expl (A : Set) (u : list A) : nat :=
  match u with
  | Nil => 0
  | Cons x u' => S (length_expl A u')
  end.

Compute length_expl nat list624.
Compute length_expl _ list624.

(** Arguments can be declared as implicit in the definition of a function *)
Fixpoint length {A : Set} (l : list A) :=
  match l with
  | Nil      => 0
  | Cons x l => S (length l)
  end.

Compute length list624.

(** If you want [A] to be an explicit parameter of Nil and Cons, 
    there is a small issue:
    it has to be given as a parameter of [Nil] and [Cons].
    However the following attempts fails.
 *)
Arguments Nil: clear implicits.
Arguments Cons: clear implicits.

Fail Fixpoint length_expl_constr (A : Set) (l : list A) :=
  match l with
  | Nil A      => 0
  | Cons A x l => S (length_expl_constr A l)
  end.

(** The error message is self-explanatory. *)
Fixpoint length_expl_constr (A : Set) (l : list A) :=
  match l with
  | Nil _      => 0
  | Cons _ x l => S (length_expl_constr A l)
  end.

(** And this is only about constructors, the defined function 
    can have implicit arguments. *)

Fail Fixpoint length_expl_constr_impl {A : Set} (l : list A) :=
  match l with
  | Nil A      => 0
  | Cons A x l => S (length_expl_constr_impl l)
  end.

(** The error message is self-explanatory. *)
Fixpoint length_expl_constr_impl {A : Set} (l : list A) :=
  match l with
  | Nil _      => 0
  | Cons _ x l => S (length_expl_constr_impl l)
  end.

Arguments Nil {A}.
Arguments Cons {A}.

(** *)

(** What we get is essentially the definition given in the standard library, 
    up to 2 minor details. *)

Print list.
Reset list.
Require Import List.
Print list.


(** We see that the name of the constructors are [nil] and [cons]
    starting with lowercase letters).  
    More importantly the type of the parameter [A] is [Type] instead 
    of [Set].  [Set] can be seen as a special case of [Type] which 
    is simpler and is actually enough most of the time, especially 
    in programming applications, since it already  allows us to 
    have lists of:
    - enumerated types, numbers...
    - user-defined datatypes, 
    - all kinds of pairs, tuples
    - lists, trees, etc. so that we have lists of lists, lists of trees
      and so on
    - functions, so that we have lists of functions of numbers,
      lists of functions of lists of tuples, etc.

    That said, [Type] becomes useful when considering lists of proofs
    (requiring [Prop] instead of [Set]) or lists of types.

    This is considered in more theoretical developments such as category 
    theory (aka "theory of abstract nonsense").
    The type system of Coq includes a "predicative hierarchy of 
    floating universes", whose complexity is hidden to the user
    through the common name "Type".

    In practice: don't bother.

    More important: the use of curly brackets around [A], making this 
    argument an implicit argument of [nil] and {cons}.
 *)

(** It is also possible to use an infix notation for lists. *)

Notation "[]" := nil.
Notation "x :: y" := (cons x y).

Definition l624' := 6 :: 2 :: 4 :: [].
Print l624'.

Import ListNotations.

Print l624'.

Definition l624  := 6 :: (2 :: (4 :: [])).
Variable l : list nat.
Definition l624'' := 6 :: 2 :: 4 :: l.


Print l624''.

(** Keep in mind that
    - as for [cons], :: is asymetric
    - ';' is misleading because it does NOT correspond to any constructor.
      If you don't understand the previous sentence, use only
      '::' and '[]'.
*)