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

[Chris Smith]

Chris Uppal wrote:
> 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.)

One question: is this more specific than simply saying that we use 
predicate logic?  A predicate divides a set into two subsets: those 
elements for which the predicate is true, and those for which it is 
false.  If we then apply axioms or theorems of the form P(x) -> Q(x), 
then we are reasoning from an "equivalence class", throwing away the 
details we don't care about (anything that's irrelevant to the 
predicate), and applying stereotypical rules (the theorem or axiom).  I 
don't quite understand what you mean by substituting classes.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation