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 -- http://mail.python.org/mailman/listinfo/python-list
