[badsock]

The "Vector m a" means that it's a vector (like a Python list) that can only be m elements long, and those elements can only be of type a. E.g. "Vector 3 Int" will always be a Vector with three integers in it. If you try to treat it like a vector of any other length it will refuse to compile (e.g. pass it to a function that requires that it have 4 or more elements).

The whole line is the type declaration for a function (app) that takes a Vector of length m, and a Vector of length n, and produces a Vector of length (m+n). Which is to say, the compiler knows at compile time what length the resulting Vector will be, and will fail to compile if the function you've written doesn't - provably - always meet that requirement.

From a Haskeller's perspective it's amazing because container types are famous loopholes for code that produces runtime errors. For instance, if you call the "head" function (returns the first element) on an empty list it will halt the program at run time with an error, despite the fact that it passed the type check (because an empty list and a full one have the same type).

As someone who learned Haskell and subsequently have been writing a lot of Python, I keep a mental tally of how many of my bugs (some of which took ages to track down) would have been caught immediately by a type system like Haskell or Idris'. I'd say it's well over half.

In Haskell those kind of errors are drastically reduced, but a few still slip through. Languages like Idris can catch even more of them, in a clever way, which is awesome.