can type system be dynamic?

In logic community, abstraction can be refined.
Type system , especially dependent type, corresponding to abstraction, so can they be make to be refined?