2 ms·
A dependent type can also just be "list of n warehouse_t", where n is completely unconstrained. I feel the constraint on the size of the input has made the disc
by Tainnor 4y ago
A dependent type can also just be "list of n warehouse_t", where n is completely unconstrained. I feel the constraint on the size of the input has made the discussion much more complicated than necessary, because now we need to carry around proof types, which are a more advanced use case.
- mcguire 4y agoTrue, 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.