4 ms·
How is that a function working on types not a macros, if that function is executed as part of the compilation process? And how is that function efficient if it
by heavenlyblue 6y ago
How is that a function working on types not a macros, if that function is executed as part of the compilation process? And how is that function efficient if it is not executed as part of the compilation?
- throwaway17_17 6y agoIt 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