Require Import natbool.

(** * Polymorphism

Previously, our [sqrt n] function was defined (more or less
arbitrarily) to return [0] when [n] is not the square of any natural
number. It's usually more desirable to have a distinct value to
represent a "no result" outcome. We can easily define a new type for
this purpose: *)

Inductive natoption := 
  | SomeNat : nat -> natoption
  | NoNat : natoption
.

(** That is, a [natoption] is either [SomeNat n] where [n] is some
number, or else it is [NoNat].

However, this is such a useful construct that we will often want to use
it with elements of other types in addition to [nat]. This is achieved
by parameterizing the definition by the type of the "some" element. *)

Inductive option A :=
  | Some : A -> option A
  | None : option A
.

(** This type is also known as [option] in ML, and [Maybe] in Haskell.

At this point it's instructive to look at the type of not only the
constructors, but of [option] itself. *)

Check option.
Check Some.
Check None.

(** We see that [option] is actually a function, although it is a
function between _types_: it takes a type [A] of elements as a
parameter, and returns the type [option A], whose values are of the form
[None A] and [Some A a], where [a : A].

The types of [Some] and [None] are also interesting: they take a type
[A] as their first argument, and the types of (the second argument and)
the result _depend_ on the particular choice of [A], in the sense
that [A] occurs in those types. The [forall] syntax is used to express a
function type with this kind of a dependence. In fact, an ordinary
function types written as [A -> B] is only syntactic sugar for [forall _
: A, B].

** Implicit arguments

Consider the term [Some nat 42]. The argument [nat] is needed in order
to specify what the type of the second argument and the result should
be. However, [42] by itself is already of type [nat], so specifying the
first argument is redundant. In fact, Coq can infer it: *)

Check (Some _ 42).

(** In a term (and not a pattern), the underscore [_] is a way of
telling Coq: "infer this argument". However, when we want Coq to
_always_ infer an argument (and we often do), we can make it
"implicit" as follows: *)

Implicit Arguments Some [A].
Implicit Arguments None [A].

(** Now we can just elide the first argument completely and Coq will
infer it. When we _do_ need to give the first argument explicitly, we
can do so by prepending the name of the function with [@]: *)

Check (Some 42).
Check (Some true).
Check (@Some nat 42).
Check (@None nat).

(** 

From the above discussion, it should be clear that types are not very
much different from other kinds of terms in Coq. A function can take a
type as a parameter, and a function can be applied to a type, and a type
even has its own type, [Type]. Nearly everything that we can do with
ordinary terms, we can also do with types, and this is part of what
gives Coq its great expressive power.



* Pairs

Continuing our quick survey on how common functional concepts are
realized in Coq, we now turn to pairs. A pair of [A] and [B] is
straightforward enough to define: the type has _one_ constructor, and
that takes _two_ arguments, of types [A] and [B], respectively.

An inductive type with a single constructor represents a kind of a
record or structure: it doesn't encode any information about choices
between alternatives, it is just a collection of elements. Coq provides
a special syntax for defining inductive types like these: *)

Structure prod A B := pair {
  fst : A;
  snd : B (* [<-] no semicolon at the end allowed *)
}.

(** The [Structure] syntax lets us name the single constructor, [pair],
and it also directly defines simple accessors to the fields of the
structure. When we print out their definitions both with pretty-printing
enabled and without it, we can see how a structure is just an inductive
type. We also see the [let]-syntax that allows easier pattern matching
on single-constructor types. *)

Print prod.
Print fst.
Set Printing All.
Print prod.
Print fst.
Unset Printing All.

(** Again, we don't want to give the type arguments explicitly all the
time since they can usually be inferred. *)

Implicit Arguments pair [A B].
Implicit Arguments fst [A B].
Implicit Arguments snd [A B].

(** The type of pairs is often called a Cartesian product, hence the
name [prod]. We provide a nice infix syntax for both the product type
and the pairs themselves. Although the syntax [A * B] is already used
for multiplication, there's no ambiguity, because this new [A * B] is
only used with types. *)

Notation "A * B" := (prod A B) : type_scope.
Notation "( a , b )" := (pair a b).

(** Just for fun, here is a simple function that reverses the elements
of a pair. It demonstrates the [let]-syntax, and one further language
feature: the parameters in braces [{A B}] are immediately made implicit.
*)

Definition swap {A B} (p : A * B) : B * A :=
  let (a, b) := p in (b, a).

(** Let's try it out: *)

Eval compute in swap (42, true).

(** 

** Sums

As a counterpart to the product types, there are sum types. An [A + B]
is either an [A] or a [B]. In Haskell, the equivalent type is known as
[Either A B]. *)

Inductive sum A B :=
  | inr : B -> sum A B
  | inl : A -> sum A B
.

Implicit Arguments inl [A].
Implicit Arguments inr [B].

Notation "A + B" := (sum A B) : type_scope.

(** **)