Re: strong/weak typing terminology (was Re: [Caml-list] Scripting in ocaml)

[Chad Perrin <perrin@apotheon.com>]

On Fri, Dec 22, 2006 at 01:21:07PM +0100, Daniel Bünzli wrote:
> Le 21 déc. 06 à 23:16, Chad Perrin a écrit :
> 
> >I mean that it doesn't allow you to go around doing in-place type
> >changes willy-nilly the way something like C does.
> 
> (Well in fact you can with Obj.magic, but that's not my point)
> 
> The problem is that this weak/strong terminology is hopelessly  
> confused (see [1],[2]). Since there is no clear unique definition of  
> strong/weak typing I think this terminology should be avoided. I tend  
> to favour the definitions you can find in the introduction of this  
> book [3] which are imho less confusing.

In point of fact, there is a clear definition.  The problem is that
people who don't pay much attention to it end up using the terms
"strongly typed" and "weakly typed" in a (ahem) weakly typed manner.
Thus, it is the colloquial definition that is almost meaningless due to
widespread conflict in its use, while there is a formal definition that
endures somewhere behind all the noise.

> 
> Basically the author distinguishes on one hand between statically and  
> dynamically typed languages, and on the other hand, between safe and  
> unsafe languages.
> 
> Static and dynamic type checking refers to whether type checks are  
> respectively performed at compilation or run time.

That's absolutely correct, and fits the formal definitions.


> 
> Safety is broadly defined as follows :
> 
> "A safe language is one that protects its own abstractions. Every  
> high-level language provides abstractions of machine services. Safety  
> refers to the language's ability to guarantee the integrity of these  
> abstractions and of higher-level abstractions introduced by the  
> programmer using the definitional facilities of the language"

That's an almost useless representation of the definition,
unfortunately, because the terms used in it are vague in application and
the structure of the definition as presented is a bit too complex.
While he may well know what he's talking about, his prose reads a bit
like poorly written code -- which is to say that it's almost unreadable
in any meaningful sense.


> 
> Later he gives the following chart
> 
>        |Statically checked       | Dynamically checked
> -------------------------------------------------
> safe   | ML, Haskell, Java, etc. | Lisp, Scheme, Perl, Postscript, etc
> unsafe | C, C++, etc.            |
> 
> Subsequently he adds :
> 
> "Language safety is seldom absolute. Safe languages often offer  
> programmers "escape hatches", such as foreign function calls to code  
> written in other, possibly unsafe, languages. Indeed such escape  
> hataches are sometimes provided in a controlled from within the  
> language itself--Obj.magic in Ocaml, ... "

He comes dangerously close to touching on strong/weak typing in that
statement.

Here's a summary of type system characteristics as I learned about them,
and confirmed by experience, research, reasoning over the years:

type-safety: A type-safe language is one whose core type system does not
allow for type errors at runtime.  Such a language is almost impossible
while still being a useful general-purpose language, but many languages
come close enough to warrant the term "type-safe" for common usage.  By
contrast, a type-unsafe language in its purest meaning is one that does
nothing to prevent type errors at all.

statically typed: A statically typed language is one that determines
types at compile time.  By contrast, a dynamically typed language is one
that determines types at runtime, generally based on context.

strongly typed: A strongly typed language is one that does not allow the
programmer to simply dodge the type system and where any instantiated or
applied datum has a given type that cannot be changed, explicitly or
implicitly.  By contrast, a weakly typed language provides casts, bit
manipulation, and other in-place conversions or evasions to subvert
types.

duck typing: This is a more recent term than others related to typing,
and arose with the Ruby community.  It essentially refers to a language
that allows for a type to be unset until the datum to be typed has a
typable value, at which point the type is "obvious" and set in stone.
The most common implementation of this uses dynamic typing, but there
are static type systems that could be called "duck typed", such as OCaml
and Objective C -- though in OCaml's case, it is achieved through type
inference, and in Objective C it is limited to object types and is
determined by behavior rather than type inference.

That's how I've come to understand type system characteristics, and it's
an internally consistent set of definitions that provides meaningful
descriptive terms and agrees with the statements of all the experts who
actually seem to care about the respective terms' meanings.  Perhaps
more to the point, it fits the computer science framework of language
theory that informs the axioms on which the best programming theory
books available (at least to judge by those I've seen).

That makes OCaml type-safe, statically typed, strongly typed, and
arguably duck typed (depending on how you use it).  It also makes Ruby
duck typed, type-safe, dynamically typed, and strongly typed; it makes
Perl type-safe, dynamically typed, and strongly typed; it makes C
statically typed, weakly typed, and kind of half-assed type-safe if
you're careful; it makes C++ less type-safe, weakly typed (though
slightly less so than C), and statically typed, as well as allowing you
to fake duck typing via templates and the like; it makes Objective C
statically typed, exactly as half-assed type-safe as C, half-assed
strongly typed (more so than C or C++), and duck typed insofar as its
object system is concerned; it makes PHP weakly typed, dynamically
typed, and type-unsafe; it makes Java fairly type-safe, weakly typed,
and statically typed; and it makes Pascal statically typed, weakly
typed, and mostly type-safe.

At least, that's what comes to mind off the top of my head.

-- 
CCD CopyWrite Chad Perrin [ http://ccd.apotheon.org ]
"Real ugliness is not harsh-looking syntax, but having to
build programs out of the wrong concepts." - Paul Graham