It is a stretched analogy and omits both practical (at the proof level) and theoretical subtlety, but you can sort of think of a dependently typed function as a

It is a stretched analogy and omits both practical (at the proof level) and theoretical subtlety, but you can sort of think of a dependently typed function as a compile time macro or a template-like generic. However, I think it would be fair to say that macros and generics are merely a mechanized implementation of a very small slice of what dependent types are capable of in full generality