> f x = f x не годится?

Это необузданная рекурсия, порождение сотоны. В нашей кошерной конструктивной логике и теории типов нет такой штуки. Благодаря чему возможно тотальное программирование, без таких вот засад. Мы можем гарантировать завершимость программ, если их типы кошерны, не ведут в ⊥.

>Чем тогда A → ⊥ не отрицание?

Это именно оно, это прямо-таки определение отрицания. Вот только инструменты в нашем конструкторе таковы, что фиг его зациклишь. Получить ⊥ можно только если его нам дали на вход или на входе есть функция, его производящая, и мы нашли, что ей скормить. Фактически, такие программы - как мысленные эксперименты, они говорят "вот если бы ты мне дал на вход такую штуку, то вот процедура, которая сделает из нее вот эту вот другую штуку". Но на практике добыть такой аргумент может быть неоткуда. В частности, функция ⊥ → ⊥ тривиальна, это id, но где взять конкретное значение типа ⊥, чтобы передать ей на вход? Построить мы эту функцию можем, это будет валидная конструкция, но вот запустить не сможем, нечего нам ей скормить.