Intuition behind encoding double negation with bottom type Nothing

Question

Shapeless encodes double negation like so

type ¬[T] = T => Nothing
type ¬¬[T] = ¬[¬[T]]

that is

(T => Nothing) => Nothing

Miles explains

...the bottom type (Scala’s Nothing type) maps to logical falsehood... negation of a type A (I’ll write it as ¬[A]) to have as it's values everything which isn’t an instance of A

Nothing is also used to represent non-termination, that is, computation that cannot produce a value

def f[T](x: T): Nothing = f(x)

Applying this interpretation to (T => Nothing) => Nothing, it seems to mean:

(          T                   =>                Nothing           )    =>          Nothing 
Assuming a value of type T,   then   the program does not terminate,   hence  it never produces a value.

Is this intuition correct? Are concepts of falsehood and non-termination equivalent? If so, why having a program that does not produce a value, which does not produce a value, means we have a value of T?

Answer 1

If so, why having a program that does not produce a value, which does not produce a value, means we have a value of T?

It doesn't. Logic arising from Curry–Howard correspondence is not classical but intuitionistic. There is no law of excluded middle T ∨ ¬T _{(but there is double negation of the law of excluded middle)}.

¬¬T is not equivalent to T.

T => ¬¬T but not ¬¬T => T.

Are concepts of falsehood and non-termination equivalent?

No. Normally non-termination is ignored. According to Curry–Howard correspondence, statement is true when corresponding type is inhabited (i.e. there is a value (term without free variables) of this type) and false when the type is not inhabited.

Nothing (or bottom type ⊥) is not inhabited (it corresponds to false). If T is inhabited then T => Nothing is not inhabited (otherwise Nothing would be inhabited). If T => Nothing is inhabited then T is not (again, otherwise Nothing would be inhabited). That's the reason to define ¬T = T => Nothing.

When non-termination is considered, this means that every type T is lifted to type T' consisting of elements of T and bottom value ⊥ (divergence, not to be confused with bottom type).