[TYPES] types

[Tamreen Khan]

Is it possible that calling them "types" in FORTRAN was just a coincidence
in that it used the same term used by Russell? I was under the impression
that types as used in that language didn't really have as much of a
mathematical basis as they do today.

Tamreen


On Tue, May 13, 2014 at 6:52 AM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
>
> Another landmark paper in the development of types as enablers is:
>
>   Jim Morris, Types are nots sets, POPL 1973. (That's the first POPL.)
>   http://dl.acm.org/citation.cfm?id=512938
>
> Yours, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ http://homepages.inf.ed.ac.uk/wadler/
>
>
> On 13 May 2014 09:12, Derek Dreyer <dreyer at mpi-sws.org> wrote:
>
> > [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> >
> > Hi Vladimir.
> >
> > I would argue that types are enabling *because* they are forbidding.
> > That sounds very zen, but I have a concrete point in mind.
> >
> > As Bob mentioned already, it was Reynolds who observed that types are
> > useful for syntactically enforcing levels of abstraction, and what
> > that really meant to Reynolds is that one can locally establish
> > invariants for -- and change private representation of -- abstract
> > data types (ADTs), without affecting the observable behavior of code
> > that relies on those types.  From my perspective, the crucial point
> > here is that types *enable* programmers to write more reliable code
> > because the burden of establishing invariants on an ADT is kept
> > *local* to the module that defines it.  The restrictions of the type
> > system then guarantee that the rest of the program, by virtue of being
> > forced to respect the abstraction of the ADT, is also forced to
> > respect the ADT's locally-established invariants.  Thus, the very
> > restrictiveness of types is what enables program *correctness* to
> > scale.
> >
> > Notice I said program correctness, not verification.  What I mean is
> > that programs written in mainstream typed languages often behave
> > correctly due to complex invariants on ADTs that the programmer has in
> > their head but that have not been written down or verified.  These
> > invariants are often really complex -- we are only now in a stage of
> > verification research where we can even begin to express them
> > formally!  But even ignoring formal verification, types have the
> > practical benefit of enabling the programmer to do some complex
> > informal reasoning locally but have confidence that it holds good when
> > the ADT is used in a much larger program.
> >
> > Best regards,
> > Derek
> >
> > On Mon, May 12, 2014 at 7:47 PM, Vladimir Voevodsky <vladimir at ias.edu>
> > wrote:
> > > [ The Types Forum,
> > http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> > >
> > > Hello,
> > >
> > > I am reading Russell's texts and the more I investigate them the more
> it
> > seems to me that the concept of types as we use it today has very little
> > with how types where perceived by Russell or Church.
> > >
> > > For them types were a restriction mechanism. As Russell and Whitehead
> > write:
> > >
> > > "It should be observed that the whole effect of the doctrine of types
> is
> > negative: it forbids certain inferences which would otherwise be valid,
> but
> > does not permit any which would otherwise be invalid."
> > >
> > > 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?
> > >
> > > Vladimir.
> > >
> > >
> > >
> > >
> > >
> >
> >
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>