I'm trying to better understand the Calculus of Constructions through Morte. My first attempt was to call the identity function itself. However,
(
λ (idType : *) →
λ (id : idType) →
(id idType))
(∀(t : *) → ∀(x : t) → t)
(λ(a : *) → λ(x : a) → x)
That program fails to compile with the error:
Context:
idType : *
id : idType
Expression: id idType
Error: Only functions may be applied to values
That doesn't make sense to me, since id is the function (λ(a : *) → λ(x : a) → x), of type idType == (∀(t : *) → t → t). Why I'm getting this error?
The problem here is that with Church-style typing (here is a nice blogpost and some discussion) everything must be well-typed from the beginning: if you have a well-typed f and a well-typed x, then you can apply f to x (if types match). If f is not well-typed, then it's not a legal term and you have an error, even if it is possible to assign f x a type.
Your λ (idType : *) → λ (id : idType) → (id idType) is not well-typed: id is a term of type idType and it's not a function that receives *, so you can't apply it to idType.