how could you possibly validate or invalidate something which doesn't exist yet? That logic cannot possibly disappear at runtime.

Supposing you write validEmail "foo@bar" :: Maybe Email, you now have to handle a case which will never happen, despite knowing as a programmer right now that this is correct. Dependent types can let you run your validation function at compile-time on the string [email protected]. Thus the logic disappeared at runtime.

Simplifying with a type like:

data NameChar = F | O
data DomainChar = B | A | R | M U
data NonEmpty = Cons a [a]
data Email = Email (NonEmpty NameChar) (NoneEmpty DomainChar)

That's a grammar for a very limited set of emails.

Then I can construct Email (Cons F (Cons O (Cons O))) (Cons B (Cons A (Cons R))) for "foo@bar" and know that it is a valid construction based on the constraints set in NameChar and DomainChar. I can also provide a validEmail :: String -> Maybe Email type for runtime construction. But I had the option to have a compile-time construct too.

Where dependent types come in in this example is that I can't, in regular Haskell, go from a string literal [Char] to the Email type without introducing partiality, because there isn't enough type information in Char to use type functions, and I don't have the ability to run code at compile time (without template-haskell). A dependent type system would let me define something like parseEmail :: (str :: [Char]) -> toType (fromStr str) where toType returns the type () if the string is invalid, and returns the type Email if valid, so that parseEmail "foo@bar" :: Email whereas parseEmail "" :: ().

See printf in Idris for a more compelling example.