Yes, but not the way you're proposing.
Just checking a vector whose size we know exactly at compile time is not difficult and does not require dependent types. We can do this in a fairly straightforward way in normal typed languages with polymorphic types.
The important insight with dependent types is that they can depend on runtime values. In your example, all the numbers (2 and 3) have to be known at compile time for the assert to work properly. Let's imagine a function zero_vec
which takes a number and gives you a vector of that length full of 0s. In a dependently typed pseudocode, this would look something like:
zero_vec : (n : ℕ) → Vec n
Note how the argument's value n
appears in the result type! In particular, zero_vec 10
would have the type Vec 10
and zero_vec 42
would have the type zero_vec 42
. More importantly, though, you could pass in a value that you don't know at runtime to zero_vec
and still typecheck your code. Imagine something like this:
n : ℕ ← readLine
zero_vec n : Vec n
You could still check this against sizes at compile time. For example, the following should work:
checkLength (zero_vec n) n
Or you should even be able to have a type like "vectors of length 3 or greater" and be able to check zero_vec n
against that too; this should give you an error since it can't prove the n
you read in is ≥ 3.
The point is that typechecking essentially becomes a pretty general form of abstract interpretation where you have to be able to propagate and check against values that you won't know until runtime.
You can't do that with your macro approach.
However, I think you can replicate dependent types with macros. The only problem is that you would essentially have to implement a whole dependent typechecker using your macro system! Which is a bit of an undertaking, but probably not as difficult as you think¹.
In fact, my understanding is that Qi and Shen are two languages implemented as Common Lisp macros with type systems as powerful as dependent types. For various reason, I've never used them (and probably never will) so I'm not sure exactly how they work.
¹ Check out "Simply Easy" for a nice tutorial.