What is Expressiveness in a Computer Language

[David Hopwood]

Anton van Straaten wrote:
> Chris Smith wrote:
> 
>> What makes static type systems interesting is not the fact that these
>> logical processes of reasoning exist; it is the fact that they are
>> formalized with definite axioms and rules of inference, performed
>> entirely on the program before execution, and designed to be entirely
>> evaluatable in finite time bounds according to some procedure or set
>> of rules, so that a type system may be checked and the same conclusion
>> reached regardless of who (or what) is doing the checking.  All that,
>> and they still reach interesting conclusions about programs.  
> 
> There's only one issue mentioned there that needs to be negotiated
> w.r.t. latent types: the requirement that they are "performed entirely
> on the program before execution".  More below.
> 
>> If informal reasoning about types doesn't meet these criteria (and it
>> doesn't), then it simply doesn't make sense to call it a type system
>> (I'm using the static terminology here).  It may make sense to discuss
>> some of the ways that programmer reasoning resembles types, if indeed
>> there are resemblances beyond just that they use the same basic rules
>> of logic.  It may even make sense to try to identify a subset of
>> programmer reasoning that even more resembles... or perhaps even is...
>> a type system.  It still doesn't make sense to call programmer
>> reasoning in general a type system.
> 
> I'm not trying to call programmer reasoning in general a type system.
> I'd certainly agree that a programmer muddling his way through the
> development of a program, perhaps using a debugger to find all his
> problems empirically, may not be reasoning about anything that's
> sufficiently close to types to call them that.  But "latent" means what
> it implies: someone who is more aware of types can do better at
> developing the latent types.

So these "latent types" may in some cases not exist (in any sense), unless
and until someone other than the original programmer decides how the program
could have been written in a typed language?

I don't get it.

> As a starting point, let's assume we're dealing with a disciplined
> programmer who (following the instructions found in books such as the
> one at htdp.org) reasons about types, writes them in his comments, and
> perhaps includes assertions (or contracts in the sense of "Contracts for
> Higher Order Functions[1]), to help check his types at runtime (and I'm
> talking about real type-checking, not just tag checking).
> 
> When such a programmer writes a type signature as a comment associated
> with a function definition, in many cases he's making a claim that's
> provable in principle about the inputs and outputs of that function.

This is talking about a development practice, not a property of the
language. It may (for the sake of argument) make sense to assign a term
such as latent typing to this development practice, but not to call the
language "latently-typed".

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>