The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

On Sat, Nov 14, 2015 at 7:45 PM, Yasuaki Kudo yasu-at-yasuaki.com |coq-club/Example Allow| <up00friojt AT sneakemail.com> wrote:

Hi,

 

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

I'm self taught in Coq. It also took me a while to understand all of the alternate syntaxes for functions and the distinction between their types and definitions.

 

 

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 .

The above line declared that F is is a function that takes a nat and returns a type of the Set sort. Function F was only declared (meaning it is assumed to exist with a given signature), it was not defined (meaning the specific implementation was not given).

I think to properly translate that line into another language, that language would need dependent typing. I know Agda and Idris have dependent types, but I don't know any more about them. Anyway if that line was translated into one of those languages, it would be so similar that I doubt it would help you understand it any better.

I'll translate it as closely as possible to C++, but C++'s type checker is not as powerful as Coq, so there is no perfect translation.

In terms of the declared but not defined aspect, that is like an extern function in C++. You can compile the code without ever giving a definition, but you can't link and run the code.

extern Set F(nat);

As I said above, C++ is not dependently typed. One can't have functions that return types (only functions that return instances of types), which is why the above line is invalid. The closest C++ has is template programming. One key difference is that in C++ all of the template code is run at compile time, but coq code could be extracted to ocaml, hooked then hooked up to user input, so that the coq code actually generates new types at runtime.

template<nat n>
struct F;

/* F is expected to be specialized for every possible nat, and every specialization should have the result field defined.

struct F<0>
{

    typedef type result;
};
*/

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

The above line declared t as an external function that takes a nat and returns an instance of F(1+x), which is a type.

template<nat x>

extern F<x>::result t();

 

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

The above line defined t' as a function that takes a nat and returns the same type returned by F(1+x). Note that the type checker automatically filled in t''s type. The above line can be equivalently written as:

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

This is also equivalent:

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

In C++, it's like this:

template<nat n>

struct t_
{

    typedef F<n + 1>::result result;

};

 

 

Check t  1.

Check F  (1+1).

Check t' 1.

 

Regards,

Yasuaki

Tokyo