What is Expressiveness in a Computer Language

[David Hopwood]

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