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