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.