The Coq mailing list

[Yves Bertot <Yves.Bertot AT inria.fr>]

On 11/15/2015 04:45 AM, Yasuaki Kudo wrote:

Hi,

 

I’m currently studying COQ (well taking a long time…) and have noticed similarities between forall (dependent product?) and function terms.

 

Although I understand they are different 😊, I wonder, in other languages or other implementations of similar ideas, can these expressions (universal quantification?) be combined as something unified?

 

Parameter  F :  nat -> Set .

Parameter  t :  forall x:nat ,  F (1+x) .

Definition t':= fun    x:nat => F (1+x).

 

Check t  1.

Check F  (1+1).

Check t' 1.

 

Regards,

Yasuaki

Tokyo

If I remember correctly, early version of Automath (starting around 1968 and into the 1970s) used lambda terms to describe the type of lambda terms.  It may be that this is also explained in the book (with explanations of other type systems).

"A modern Perspective on Type Theory From its Origins Until Today", Applied Logic Series, Vol. 29, 357.

F. Kamareddine, T. Laan, and R. Nedepelt (2004) ISBN 1-4020-2334-0.

I tried to read this book, but I did not find the time to go beyond the first few pages, so my pointer may be wrong.

Yves