QED 16: Elements

Share:

Listens: 0

Q.E.D. Code

Technology


Euclid's Elements takes a disciplined, formal approach to proving assertions based only on simple axiomatic statements. While most of these axioms are elegant, one of them is more complex and wordy. It seems as if it should be provable from the others. Several mathematicians have tried, but eventually they found a surprising result. Beware when proving your own assertions that you don't make the mistake of assuming something that seems obvious. Category theory isn't as complex as you might be lead to believe. A category is nothing more than a contract that sets rules on how a type is to behave. Functors, despite having a weird name, are just types that can map functions into a different space. The List type is an example of a functor, because it can transform a function on its elements into a function on lists. And Applicatives are just wrapper types. They are especially useful for building pipelines. CQRS, Command Query Responsibility Segregation, is a pattern that applies the Single Responsibility Principle to components such that they either change the system (commands), or observe it (queries). Segregation alone gives us the ability to prove some very useful things about a system: safety, determinism, and consistency for example. But it does not prescribe asynchrony or eventual consistency. Those are architectural decisions left to you.