I have been talking to some computer language designers and have come up against an old conundrum that is interfering in explaining to people the language features that it seems easy to explain to the computer, in the form of writing a compiler.
<p>
The conundrum is whether we invented or discovered some new mathematical concept such as rational number.
<a href=http://en.wikipedia.org/wiki/Leopold_Kronecker>Kronecker</a> gained fame from saying that the integers were by God and the rest [invented] by man.
<p>
The conundrum is even baser:<ul>

In the language context I want to write a program and invent a type of record whose fields I can read and write.
I also want to pass these records to a sort routine but deny that routine the ability to do anything with these records but compare two records to see if the keys are equal, less or greater.
(Imagine sorting employee records on salary.)
The sort routine, which was completed before my project began, was compiled in the context of a type declaration of ‘Record’ and a function RCmp(r1, r2), to compare two Records and returning a (=, <, >) value.</ul>

To call the sort routine I need to name the type of the parameter that names the record that I will receive.
I also need the name of a routine to compare such records.
<p>Just now (2013 Mar 31) I think one answer is existential types where I can say that for each invocation of the block containing this declaration there will exist a type t and a routine c of type t → t → bool.
That allows me to declare variables, parameters, arrays and lists of type t and call a routine c declared to take two references to a t and receive back a (=, <, >) report.
<p>I am not entirely sure that existential types can come in from the cold to be first class types.