Joe Marshall wrote:
> 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).
Yes, see the correction in my follow-up.
>>>>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.
I don't think you've shown that. I would like to see a more explicit
construction of a dynamically typed [*] program with a given specification,
where it is not possible to write a statically typed program that meets
the same specification using the same algorithms.
AFAIK, it is *always* possible to construct such a statically typed
program in a type system that supports typerec or gradual typing. The
informal construction you give above doesn't contradict that, because
it depends on reflecting on a [static] type system, and in a dynamically
typed program there is no type system to reflect on.
[*] Let's put aside disagreements about terminology for the time being,
although I still don't like the term "dynamically typed".
> 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,
I don't know, it would probably have more entertainment value than most
executive toys :-)
> but there should be programs that are independently non
> checkable against a sufficiently powerful type system.
Why?
Note that I'm not claiming that you can check any desirable property of
a program (that would contradict Rice's Theorem), only that you can
express any dynamically typed program in a statically typed language --
with static checks where possible and dynamic checks where necessary.
--
David Hopwood <[EMAIL PROTECTED]>
--
http://mail.python.org/mailman/listinfo/python-list
