[TYPES] types

[Derek Dreyer]

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