The proof and interpretation of Gantō's axe in Haskell

GantoAxe.hs

-- see https://blog.plover.com/math/logic/gantos-axe.html

import Data.Void

-- The general theorem, valid for all types p, q
heart :: (p -> q) -> ((p -> Void) -> q) -> (q -> Void) -> Void
-- The proof
heart pq npq nq = v where
    -- np :: p -> Void
    np = nq . pq
    -- qq :: q
    qq = npq np
    -- v :: Void
    v = nq qq

-- Now, its validity for some specific pairs of types:

-- It is valid for two inhabited types (e.g. Int, String):
heartIS :: (Int -> String) -> ((Int -> Void) -> String) -> (String -> Void) -> Void
heartIS pq npq nq = nq $ npq $ nq . pq
-- Why is it valid? Because while you can provide the first two functions,
-- there is no way you can provide the *third* function, the String -> Void type is uninhabited:
-- heartIS (const "") (const "") *impossible*

-- It is valid for the first inhabited and the second uninhabited (Int, Void):
heartIV :: (Int -> Void) -> ((Int -> Void) -> Void) -> (Void -> Void) -> Void
heartIV pq npq nq = nq $ npq $ nq . pq
-- Why? Because while you can provide the second two functions, you cannot provide the *first* one,
-- the Int -> Void type is uninhabited:
-- heartIV *impossible* ($ 3) id

-- It is valid for the first uninhabited and the second inhabited (Void, Int):
heartVI :: (Void -> Int) -> ((Void -> Void) -> Int) -> (Int -> Void) -> Void
heartVI pq npq nq = nq $ npq $ nq . pq
-- Why? Because while you can provide the first two functions, there is no way you can provide
-- the *third* function, the Int -> Void type is uninhabited:
-- heartVI (const 3) (const 3) *impossible*

-- It is valid for two uninhabited types (Void, Void):
heartVV :: (Void -> Void) -> ((Void -> Void) -> Void) -> (Void -> Void) -> Void
heartVV pq npq nq = nq $ npq $ nq . pq
-- Why? Because you cannot provide the second function in this case, the ((Void -> Void) -> Void)
-- type is uninhabited:
-- heartVV id *impossible* id


-- To be sure, let us check the correctness of the inhabitated types for each case:
-- When we remove the problematic argument in each case, the rest could be provided easily
-- (and the result would be true (inhabited)).
heartISCheck :: (Int -> String) -> ((Int -> Void) -> String) -> String
heartISCheck pq npq = "OK"
checkHeartISCheck = heartISCheck (const "") (const "") 

heartIVCheck :: ((Int -> Void) -> Void) -> (Void -> Void) -> String
heartIVCheck npq nq = "OK"
checkHeartIVCheck = heartIVCheck ($ 3) id

heartVICheck :: (Void -> Int) -> ((Void -> Void) -> Int) -> String
heartVICheck pq npq = "OK"
checkHeartVICheck = heartVICheck (const 3) (const 3)

heartVVCheck :: (Void -> Void) -> (Void -> Void) -> String
heartVVCheck pq nq = "OK"
checkHeartVVCheck = heartVVCheck id id

main :: IO ()
main =  do
    putStrLn checkHeartISCheck
    putStrLn checkHeartIVCheck
    putStrLn checkHeartVICheck
    putStrLn checkHeartVVCheck