2. Why does the open and closed principle only have to apply to code? What if it could apply to everything. You gain benefits when you apply this concept to code... what is stopping the benefits from transferring over to runtime structures. SOLID for OOP is defined in an abstract hand wavy way, for FP many of those guidelines become concrete laws of the universe.
>No type checker is mathematically sound.
3. A type checker proves type correctness. Languages can go further with automated provers like COQ or agda. They are mathematically sound. Your square example just means that types shouldn't be defined that way. It means that the type checker isn't compatible with that method of defining types.
5. I highly disagree. There should only be communication between modules NEVER dependency injection. The monthly activity module should not even accept ANY module, or module interface as a parameter. It should only accept the OUTPUT of that module as a parameter. This makes it so that there are ZERO dependencies.
For example don't create a Car object that takes in an engine interface. Have the engine output joules as energy and have the car take in joules to drive. Function Composition over Dependency Injection. (Also think about how much easier it is to unit test Car without a mock engine)
If you get rid of dependency injection, you get rid of the dependency inversion principle. DIP builds upon a very horrible design principle which makes the entire principle itself horrible.