What is Expressiveness in a Computer Language

[Ketil Malde]

Chris Smith <cdsmith at twu.net> writes:

> Joachim Durchholz <jo at durchholz.org> wrote:
>> Assume a language that
>> a) defines that a program is "type-correct" iff HM inference establishes 
>> that there are no type errors
>> b) compiles a type-incorrect program anyway, with an establishes 
>> rigorous semantics for such programs (e.g. by throwing exceptions as 
>> appropriate).

> So the compiler now attempts to prove theorems about the program, but 
> once it has done so it uses the results merely to optimize its runtime 
> behavior and then throws the results away. 

Hmm... here's my compiler front end (for Haskell or other languages
that ..er.. define 'undefined'):

  while(type error) {
    replace an incorrectly typed function with 'undefined'
  }

Wouldn't the resulting program still be statically typed?

In practice I prefer to (and do) define troublesome functions as
'undefined' manually during development.

-k
-- 
If I haven't seen further, it is by standing in the footprints of giants