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?
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.