1ML doesn&#x27;t really unify the type and value languages. First-class modules are syntactic sugar over System F-omega, which means that the elaboration&#x2F;type-checking phase of 1ML duly splits modules into type and value components, which live in separate worlds.<p>Personally, I find 1ML&#x27;s approach more pragmatic, or, at least, easier to digest for most programmers - including Haskell programmers. Dependent types are more powerful, but they aren&#x27;t free from complications. For instance, unifying the type and value languages willy-nilly can cause trouble if you want your value language to be Turing-complete, because now type-level computation can diverge too! In a language based on System F-omega, type-level computation is guaranteed not to diverge, because its type level is the simply typed lambda calculus. Some use cases might warrant providing more powerful type-level computation facilities (e.g. calculating the shapes of multidimensional matrices), but it isn&#x27;t clear to me that the full power of a Martin-Loef-style dependent type theory is needed.