David Hopwood wrote: > Joe Marshall wrote: > > > (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 #' is just a namespace operator. The function accepts a single argument and returns the function itself. You need a type that is a fixed point (in addition to the universally quantified argument). > >>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." Presumably the remainder of the program does something interesting! The point is that there exists (by construction) programs that can never be statically checked. The next question is whether such programs are `interesting'. Certainly a program that is simply designed to contradict the type checker is of limited entertainment value, but there should be programs that are independently non checkable against a sufficiently powerful type system. -- http://mail.python.org/mailman/listinfo/python-list
