search

braibant / articheck

14 stars 2 forks source link

Start thinking about a vocabulary #18

Closed protz closed 10 years ago

protz commented 10 years ago

I've commented everything up to the RBT example in the source code. I believe it constitutes a good starting point for the explanations we'll have to provide in the paper about the thing.

We should consider settling on a vocabulary for the things we manipulate. I've abused the word "descriptor" in the comments: 'a ty is a descriptor of type t, while ('b, 'a) fn describes functions with type 'b that generate elements of type 'a. Sig.t describes module signatures that we wish to test.

Comments are welcome.

braibant commented 10 years ago

+1 for type descriptor.

I would like to find a proper name for ('a,'b) fn. I used to think of them as "morphism declaration" in Coq terms, or "proper morphisms" as they are called. However, this is not really palatable. What about declaration of function signature that we abridge in the following as function signature.

gasche commented 10 years ago

There are significant changes to the vocabulary in the stlc branch (see pull request #19). In any case I definitely agree that we should try to be consistent.