[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Mon, May 12, 2014 at 1:47 PM, Vladimir Voevodsky <[email protected]>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 to programming languages, but I think an interesting aspect of the types-as-enabling story goes back to Goedel's System T, from the Dialectica paper of the early 1950s. 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 added, 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. Joshua
