Could you elaborate why the author should use a broader term? Refinement Types is an even broader category than dependent types, and do not necessarily include types which depend on a value. In this case the author is specifically referring to types which depend on a value.
In his example he’s not encoding the length of the arrays into the type, just adding a type contract that the length of the output of the function matches the lengths of the inputs. This is more in line with how refinement type systems work than dependent type systems.
I think the author is conflating dependent types and refinement types.
Could you elaborate why the author should use a broader term? Refinement Types is an even broader category than dependent types, and do not necessarily include types which depend on a value. In this case the author is specifically referring to types which depend on a value.
In his example he’s not encoding the length of the arrays into the type, just adding a type contract that the length of the output of the function matches the lengths of the inputs. This is more in line with how refinement type systems work than dependent type systems.
The author mentions a few languages toward the end, but forgets one of my favourite languages: http://www.ats-lang.org/