Re: [TYPES] types

[ 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 <[email protected]> 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 <[email protected]>
> 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.