What is Expressiveness in a Computer Language

[Joe Marshall]

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.