Formal Language

A formal language over some set of symbols $\Sigma$ is a subset of the Power Set $\mathcal{P}(\Sigma^{*})$ of Lists of elements of $\Sigma$. Type theoreticall, this is just a predicate $\mathsf{List}\;\Sigma\to\Omega$.