[TYPES] types

[Joshua Guttman]

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
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