5 ms·
Nobody's mentioned dependent typing yet, but languages like Idris and Agda will "narrow types based on control flow" (in fact, since they're pure-functional, co
by chriswarbo 5y ago
Nobody's mentioned dependent typing yet, but languages like Idris and Agda will "narrow types based on control flow" (in fact, since they're pure-functional, control-flow is the same as data-flow). For example, zipping two vectors of the same length:
zip: Vec n t1 -> Vec n t2 -> Vec n (t1, t2)
zip Nil Nil = Nil
zip (Cons x xs) (Cons y ys) = Cons (x, y) (zip xs ys)
Here the 'Vec' type has two constructors, Nil and Cons. Since their types specify the same length, the type-checker knows we can ignore the 'zip Nil Cons' or 'zip Cons Nil' cases.
- alduin32 5y agoThis is amazing, but I don't understand the justification : > Since their types specify the same length, the type-checker knows we can ignore the 'zip Nil Cons' or 'zip Cons Nil' cases. Specifically, I have trouble understanding "their types specify the same length". Whose types ?
- masklinn 5y agoThe types of the vectors: the length is a generic parameter to the type. So a Vec 4 Int and a Vec 5 Int are different types.
- alduin32 5y agoOh right, the output is parametrized by the input. I suppose this is what dependent types are. That's really awesome. Thanks for the explanation.
- masklinn 5y ago> Oh right, the output is parametrized by the input. I suppose this is what dependent types are. Dependent types is really about the ability to parameterise types over values, and reason on those values-dependent types.
- earleybird 5y agoYou might read the Vector type constructor 'Vector N T' as "this is a Vector of T's of length N'.