> With dynamic typing you can easily manipulate types as objects There are statically typed languages like Agda in which types themselves are "first-class obje

> With dynamic typing you can easily manipulate types as objects There are statically typed languages like Agda in which types themselves are "first-class objects" whose types are "kinds" whose types are "sorts" and so on. They form a hierarchy of Russel universes where functions can be defined at every level of the hierarchy. Typical ambiguity even allows to define implicitly universe-polymorphic functions that work on terms of every universe, i.e. you can write a function that can be applied to values _or_ types _or_ kinds just the same.