3 ms·
True, but at that point you're not using dependent types.
by mcguire 4y ago
True, but at that point you're not using dependent types.
- Tainnor 4y agoYou are, because the type still depends on the value of n. It's just that that value is unconstrained. It can still be used parametrically in type signatures, though, e.g. append : Vect n a -> Vect m a -> Vect (n+m) a That's not possible without dependent types.