The only reason why Haskell uses (::) is because they wanted to preserve (:) for lists, thinking that list operations would be more prevalent than type operatio

The only reason why Haskell uses (::) is because they wanted to preserve (:) for lists, thinking that list operations would be more prevalent than type operations. That ended up being a poor bet, as it turns out. (:) is very standard notation for "has type" in type theory. Also, all of the mapN functions exist in Haskell and Idris as applications of the Applicative typeclass.