Coming from traditional statically typed languages (Java, C++, Typescript, even Python or Ruby...), you might think of a type like "int" or "Float". He's calling stamps "micro-types" because they're more fine-grained than that. A stamp might tag a value as being between 0 and 255, for example, which is much more specific than "int".

It would be really cool to work with a language that allows the user such fine-grained types, which is one reason I keep eyeing Idris.