There are no dynamic types, but there may be dynamic typing. All those so called dynamic typed languages are actually statically uni-typed and figure out at run time the so called dynamic type.
Types are not properties of data, types are proofs about your program. In general type safety provides proofs of preservation of types and that your program won't get stuck due to types.
The perception you have about types is exactly the problem that Prof Harper is trying to avoid in his students.
Then maybe all this conflict really is "a problem of grammar", as Harper himself asserts. For me, the word type has a differenn meaning than for you. Maybe we should instead be using the expressions static type (compile-time proof) and dynamic type (runtime properties of data, which Harper calls class, though I prefer not to use this word as its meaning is already too overloaded in CS).
What you're calling a dynamic type is what he'd call a canonical form. If your typing system has product types, then you should be able to prove that anything with a product type evaluates down to an ordered pair.
Comments
There are no dynamic types, but there may be dynamic typing. All those so called dynamic typed languages are actually statically uni-typed and figure out at run time the so called dynamic type. Types are not properties of data, types are proofs about your program. In general type safety provides proofs of preservation of types and that your program won't get stuck due to types. The perception you have about types is exactly the problem that Prof Harper is trying to avoid in his students.
Then maybe all this conflict really is "a problem of grammar", as Harper himself asserts. For me, the word type has a differenn meaning than for you. Maybe we should instead be using the expressions static type (compile-time proof) and dynamic type (runtime properties of data, which Harper calls class, though I prefer not to use this word as its meaning is already too overloaded in CS).
What you're calling a dynamic type is what he'd call a canonical form. If your typing system has product types, then you should be able to prove that anything with a product type evaluates down to an ordered pair.