News for hackers. Stuff that matters.

A comment on Why don't more languages offer flow typing?. Parent comment

Re:Why don't more languages offer flow typing? by alduin32 on Monday April 04, 2022 @03:57PM (#30911300)
This 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 ?

[ Parent | on HN ]
Re:Why don't more languages offer flow typing? by masklinn on Monday April 04, 2022 @04:41PM (#30911705)
The 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.
[ Parent | on HN ]
Re:Why don't more languages offer flow typing? by alduin32 on Monday April 04, 2022 @11:43PM (#30915086)
Oh right, the output is parametrized by the input. I suppose this is what dependent types are.

That's really awesome. Thanks for the explanation.

[ Parent | on HN ]
Re:Why don't more languages offer flow typing? by masklinn on Tuesday April 05, 2022 @02:33AM (#30915921)
> 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.

[ Parent | on HN ]
Re:Why don't more languages offer flow typing? by earleybird on Monday April 04, 2022 @05:07PM (#30911933)
You might read the Vector type constructor 'Vector N T' as "this is a Vector of T's of length N'.
[ Parent | on HN ]