Saying "latently-typed language" is making a category mistake

[Chris Uppal]

Chris Smith wrote:

> Perhaps, if you wanted to be quite careful about your distinctions, you
> may want to choose different words for the two.  However, then you run
> into that same pesky "you can't choose other people's terminology" block
> again.

There may be more flexibility in this area than you'd think.  I get the
impression that (after only a few years hard work) the terms "weak typing" and
"strong typing", used as synonyms for what we are here calling "dynamic typing"
and "static typing", are starting to die out.

So be of good hope !

I may yet be persuaded to talk of "static type checks" vs "dynamc checks" (with
a slight, veilled, sneer on the word "type" -- oh, so very limiting ;-)


> I'd be more careful in the analogy, there.  Since type theory (as
> applied to programming languages, anyway) is really just a set of
> methods of proving arbitrary statements about program behaviors,

Not "arbitrary" -- there is only a specific class of statements that any given
type system can address.  And, even if a given statement can be proved, then it
might not be something that most people would want to call a statement of type
(e.g. x > y).


It seems to me that most (all ?  by definition ??)  kinds of reasoning where we
want to invoke the word "type" tend to have a form where we reduce values (and
other things we want to reason about) to equivalence classes[*] w.r.t the
judgements we wish to make, and (usually) enrich that structure with
more-or-less stereotypical rules about which classes are substitutable for
which other ones. So that once we know what "type" something is, we can
short-circuit a load of reasoning based on the language semantics, by
translating into type-land where we already have a much simpler calculus to
guide us to the same answer.

(Or representative symbols, or...  The point is just that we throw away the
details which don't affect the judgements.)


> a
> corresponding "informal type theory" would just be the entire set of
> informal reasoning by programmers about their programs.

I think that, just as for static theorem proving, there is informal reasoning
that fits the "type" label, and informal reasoning that doesn't.

I would say that if informal reasoning (or explanations) takes a form
more-or-less like "X can [not] do Y because it is [not] a Z", then that's
taking advantage of exactly the short-cuts mentioned above, and I would want to
call that informal type-based reasoning.  But I certainly wouldn't call most of
the reasoning I do type-based.

    -- chris