GADTs let you do similar things in the simplest cases, they just don't work as well for complex constraints.
Like, append: Vector n t -> Vector m t -> Vector (n+m) t. With GADTs you need to manually lift (+) to work on the types, and then provide proofs that it's compatible with the value-level.
Then you often need singletons for the cases that are more complex- if I have a set of integers, and an int x, and I want to constrain that the item is in the set and is also even, the GADT approach looks like:
doThing ::
Singleton Int x
-> Singleton (Set Int) s
-> IsInSet x s
-> IsEven x
-> SomeOutput
Which looks reasonable, until you remember that the Singleton type has to have a representation which is convenient to prove things about, not a representation that is convenient/efficient to operate on, which means your proofs will be annoying or your function itself will hardly resemble a "naive" untyped implementation.
Dependent types fix this because your values are "just" values, so it would be something like
doThing ::
(x : int)
-> (s : set int)
-> so (is_in s x)
-> so (even x)
-> SomeOutput
Here, x and s are just plain values, not a weird wrapper, and is_in and event are ordinary (and arbitrary) library functions.
Like, append: Vector n t -> Vector m t -> Vector (n+m) t. With GADTs you need to manually lift (+) to work on the types, and then provide proofs that it's compatible with the value-level.
Then you often need singletons for the cases that are more complex- if I have a set of integers, and an int x, and I want to constrain that the item is in the set and is also even, the GADT approach looks like:
doThing :: Singleton Int x -> Singleton (Set Int) s -> IsInSet x s -> IsEven x -> SomeOutput
Which looks reasonable, until you remember that the Singleton type has to have a representation which is convenient to prove things about, not a representation that is convenient/efficient to operate on, which means your proofs will be annoying or your function itself will hardly resemble a "naive" untyped implementation.
Dependent types fix this because your values are "just" values, so it would be something like
doThing :: (x : int) -> (s : set int) -> so (is_in s x) -> so (even x) -> SomeOutput
Here, x and s are just plain values, not a weird wrapper, and is_in and event are ordinary (and arbitrary) library functions.