joshua.guttman at gmail.com
Tue May 13 13:21:30 EDT 2014
On Mon, May 12, 2014 at 1:47 PM, Vladimir Voevodsky <vladimir at ias.edu>wrote:
> The types which we use today are a constructive tool. For example, types
> in Ocaml are a device without which writing many programs would be
> extremely inconvenient.
> I am looking for a historic advice - when and where did types appear in
> programming languages which were enabling rather than forbidding in nature?
I'm not really sure whether this was historically influential when it comes
programming languages, but I think an interesting aspect of the
story goes back to Goedel's System T, from the Dialectica paper of the
Having the structure of simple types, together with the primitive recursion
operators of all types to fill in the functions in a somewhat finitist way:
This seems to me an interesting start on a notion of computation where
the types are central, and the means for generating computational activity
tightly hew to the type structure.
By the 70s, I guess a lot of people were aware that with pairing types
it was a pretty appealing framework. And the addition of sum types or
primitive recursive sum types seems pretty obvious.
But I don't know whether Reynolds or Milner etc were aware of this
corner of the proof theory literature. It was certainly not available in
English in the late 70s.
More information about the Types-list