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.

The conundrum is whether we invented or discovered some new mathematical concept such as rational number. Kronecker gained fame from saying that the integers were by God and the rest [invented] by man.

The conundrum is even baser:

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.

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.

I am not entirely sure that existential types can come in from the cold to be first class types.