unit, top, bottom

Thank you for your criticism. If I'm not missing anything, Haskell's () and Void type corresponds to the unit and bottom type respectively. What would the top type be in Haskell?

Hmm, interesting point.

Propositional logic, and first order logics are both sound, and complete

From the wikipedia article of Godel's Completeness Theorem,

The completeness theorem applies to any first-order theory: If T is such a theory, and φ is a sentence (in the same language) and every model of T is a model of φ, then there is a (first-order) proof of φ using the statements of T as axioms. One sometimes says this as "anything universally true is provable". This does not contradict Gödel's incompleteness theorem, which shows that some formula φu is unprovable although true in the natural numbers, which are a particular model of a first-order theory describing them — φu is just false in some other model of the first-order theory being considered (such as a non-standard model of arithmetic for Peano arithmetic). This kind of failure of consistency between a standard and non-standard model is also called Omega Inconsistency.

My interpretation is that propositional logic is complete, but propositional logic is incomplete when you consider facts about propositional logic.