What is Expressiveness in a Computer Language

[David Hopwood]

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 <david.nospam.hopwood at blueyonder.co.uk>