But there are a few languages that have both, such as Ur and Coq, and possibly others. Also, I know that there&#x27;s work on a more powerful module system for Haskell called Backpack (although, I&#x27;m not really familiar with it). I agree that there are certain conceptual incompatibilities between the two as you mention, but they&#x27;re both so useful that it seems like there must be good ways to bring them together, or at least make both of them available.