Joe Marshall wrote: > It isn't clear to me which programs we would have to give up, either. > I don't have much experience in sophisticated typed languages. It is > rather easy to find programs that baffle an unsophisticated typed > language (C, C++, Java, etc.). > > Looking back in comp.lang.lisp, I see these examples: > > (defun noisy-apply (f arglist) > (format t "I am now about to apply ~s to ~s" f arglist) > (apply f arglist))
'noisy-apply' is typeable using either of these systems: <http://www.cs.jhu.edu/~pari/papers/fool2004/first-class_FOOL2004.pdf> <http://www.coli.uni-saarland.de/publikationen/softcopies/Muller:1998:TIF.pdf> (it should be easy to see the similarity to a message forwarder). > (defun blackhole (argument) > (declare (ignore argument)) > #'blackhole) This is typeable in any system with universally quantified types (including most practical systems with parametric polymorphism); it has type "forall a . a -> #'blackhole". >>The real question is, are there some programs that we >>can't write *at all* in a statically typed language, because >>they'll *never* be typable? > > Certainly! As soon as you can reflect on the type system you can > construct programs that type-check iff they fail to type-check. A program that causes the type checker not to terminate (which is the effect of trying to construct such a thing in the type-reflective systems I know about) is hardly useful. In any case, I think the question implied the condition: "and that you can write in a language with no static type checking." [...] >>>If you allow Turing Complete type systems, then I would say no--every >>>bug can be reforumlated as a type error. If you require your type >>>system to be less powerful, then some bugs must escape it. >> >>I don't think so. Even with a Turing complete type system, a program's >>runtime behavior is still something different from its static behavior. >>(This is the other side of the "types are not tags" issue--not only >>is it the case that there are things static types can do that tags >>can't, it is also the case that there are things tags can do that >>static types can't.) > > I agree. The point of static checking is to *not* run the program. If > the type system gets too complicated, it may be a de-facto interpreter. The following LtU post: <http://lambda-the-ultimate.org/node/1085> argues that types should be expressed in the same language that is being typed. I am not altogether convinced, but I can see the writer's point. There do exist practical languages in which types can be defined as arbitrary predicates or coercion functions, for example E (www.erights.org). E implementations currently perform type checking only at runtime, however, although it was intended to allow static analysis for types that could be expressed in a conventional static type system. I think the delay in implementing this has more to do with the E developers' focus on other (security and concurrency) issues, rather than an inherent difficulty. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list