What is Expressiveness in a Computer Language

[Joachim Durchholz]

rossberg at ps.uni-sb.de schrieb:
> Joachim Durchholz write:
>> Another observation: type safeness is more of a spectrum than a clearcut
>> distinction. Even ML and Pascal have ways to circumvent the type system,
> 
> No. I'm not sure about Pascal,

You'd have to use an untagged union type.
It's the standard maneuver in Pascal to get unchecked bitwise 
reinterpretation.
Since it's an undefined behavior, you're essentially on your own, but in 
practice, any compilers that implemented a different semantics were 
hammered with bug reports until they complied with the standard - in 
this case, an unwritten (and very unofficial) one, but a rather 
effective one.

 > but (Standard) ML surely has none.

NLFFI?

 > Same with Haskell as defined by its spec.

Um... I'm not 100% sure, but I dimly (mis?)remember having read that 
UnsafePerformIO also offered some ways to circumvent the type system.

(Not that this would be an important point anyway.)

 > OCaml has a couple of clearly
> marked unsafe library functions, but no unsafe feature in the language
> semantics itself.

If there's a library with not-typesafe semantics, then at least that 
language implementation is not 100% typesafe.
If all implementations of a language are not 100% typesafe, then I 
cannot consider the language itself 100% typesafe.

Still, even Pascal is quite a lot "more typesafe" than, say, C.

>> and even C is typesafe unless you use unsafe constructs.
> 
> Tautology. Every language is "safe unless you use unsafe constructs".

No tautology - the unsafe constructs aren't just typewise unsafe ;-p

That's exactly why I replaced Luca Cardelli's "safe/unsafe" 
"typesafe/not typesafe". There was no definition to the original terms 
attached, and this discussion is about typing anyway.

> (Unfortunately, you can hardly write interesting programs in any safe
> subset of C.)

Now that's a bold claim that I'd like to see substantiated.

>> IOW from a type-theoretic point of view, there is no real difference
>> between their typesafe and not typesafe languages in the "statically
>> typed" column; the difference is in the amount of unsafe construct usage
>> in practial programs.
> 
> Huh? There is a huge, fundamental difference:  namely whether a type
> system is sound or not.

I think you're overstating the case.

In type theory, of course, there's no such things as an "almost typesafe 
language" - it's typesafe or it isn't.

In practice, I find no implementation where type mismatches cannot 
occur, if only when interfacing with the external world (except if you 
cheat by treating everything external as a byte sequence, which is like 
saying that all languages have at least a universal ANY type and are 
hence statically-typed).
And in those languages that do have type holes, these holes may be more 
or less relevant - and it's a *very* broad spectrum here.
And from that perspective, if ML indeed has no type hole at all, then 
it's certainly an interesting extremal point, but I still have a 
relevant spectrum down to assembly language.

Regards,
Jo