[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Matthias Felleisen wrote: > Furthermore, you can use typed thinking to organize the design of programs > even in the absence of a type language and type checking. I have run courses > for over 20 years this way and successfully so from the middle school level to > the MS level. More concretely, you can program with types in "Scheme"; you > don't need to be in "Ocaml" (quotes to remind readers that I mean the idea, > not > the exact language). Indeed, given the huge demand for "untyped" programmers, > I argue that a responsible instructor must expose students to just such > scenarios to prepare his students for this world. Greg Morrisett wrote: > 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. What is strange here that even if a language is untyped, and I cannot put enough quoting marks here, the programmer is thinking using types, even in e.g. Javascript, and it is more difficult to teach it not mentioning types. One should refer to the compiler that makes something dubious with types. Of course Javascript is more written than read and that is easier without explicit types. - Gergely
