[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I seem to vaguely recall that in the remote past, types in some programming languages were called "modes" (Algol?). So to find the literature before types in logic and in programming languages "converged" one probably has to look for that keyword. M.
On 13/05/14 15:25, Greg Morrisett wrote:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] One thing this whole conversation ignores is the role of types in compilation. Even early FORTRAN compilers needed to make distinctions (integral versus floating-point) in order to (a) determine how much space to allocate, (b) [possibly] align values in memory, and (c) to dispatch to appropriate instructions for doing arithmetic (i.e., "+" was overloaded.) These distinctions are still relevant and important today. Indeed, types have played a central role in efficient compilation of languages, and in that sense, are extremely enabling. A uni-typed language, in the parlance of Harper, requires a universal representation, which usually means a level of indirection, perhaps additional tags so that we can discriminate, etc. Today, a good compiler for a uni-typed language first reconstructs the underlying "Scott-types" (or some refinement thereof) in the hopes of avoid the costs of universal representations. (See e.g., the JVML, LLVM, GHC's IR, etc.) So the practice and theory are quite aligned here: types form the foundations, and the illusion of a dynamically-typed setting is there for convenience of the user. Even in the uni-typed languages, not all operations are allowed on all values (e.g., trying taking the car/head of a lambda), even though these operations are certainly defined at the bit-level. So there is some imposition of abstraction before the fact, enabling reasoning at the level of the language's abstract machine, instead of the concrete bit-level. I suppose if you turn your head around backwards enough, you see this as an "imposition" on your God-given right to do what you want with the bits, but others see this as a constructive way to define a language. -Greg
-- Martin Escardo http://www.cs.bham.ac.uk/~mhe
