I appreciate this article. It's clear, easy to understand, and uses theory to propose practical improvements to FP.

Some minor nitpicks:

> In total functional programming ⊥ does not exist.

That doesn't seem right. In total FP, we can still define a ⊥ type that has no values. I think the problem here is that the author uses ⊥ to indicate both a type and a value of that type (e.g. f ⊥ = ⊥), which is confusing.

> 0 / 0 = 0

Surely it would be better to use a Maybe type for this instead?

    0 / 1 = Just 0
    0 / 0 = Nothing

The same approach also addresses the difficulty of hd:

    hd :: List a -> Maybe a
    hd (Cons a x) = Just a
    hd Nil = Nothing

F# has this function, and calls it "tryHead", rather than just "head".