Check cnat. and got Type return

Question

All

I am trying to understand the Church numerals, mentioned in the SF-LF book, chp4.

Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition one : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.
Check cnat.
Check one.

And I get

cnat
     : Type
one
     : cnat

It seems cnat is some kind of type, and function at the same time. How can it be both type and function? Anyone can help explain a little more about this?

Answer 1

The "forall (X : Type)," syntax is a way to form a type, from a type parameterized by X. forall (X : Type), (X -> X) -> X -> X is a type of functions, which given a type X produce a value of type (X -> X) -> X -> X (which is itself a function).

The "fun (X : Type) =>" syntax is a way to form a function, from a term parameterized by X. fun (X : Type) (f : X -> X) (x : X) => f x is a function, which given a type X produce the function fun (f : X -> X) (x : X) => f x (which is itself a function).

What fun and forall have in common is that they involve binders, like (X : Type) (also like (f : X -> X), (x : X)). fun is a construct that involves binders to form functions, but not all constructs that involve binders form functions: forall is a construct that involves binders to form types.