Russell's paradox in Idris is
\[ type : Type \]
\[ type = Type \]
In the first line I say that I'm going to define a type named "type". In the second line I assign this type to be the type of all types. Is Russell rolling in his grave because this compiles?

@JadeMasterMath There's a lot of fun history there... Russell's paradox requires comprehension which you don't have in type theory. Martin-Löf's original type theory had Type : Type, which turns out to be inconsistent but for a different reason, that was discovered by Girard so it gets called Girard's paradox

Actually I have absolutely no idea how to prove Girard’s paradox, ie. to construct an inhabitant of the empty type starting from the Type : Type axiom

@julesh @JadeMasterMath So unless you remember how to pony up a term of type Zero (or whatever they call the empty type in Idris; tell me it's not Void; it's Void, isn't it? I want to kill myself; no; I want to kill whoever called it Void), you don't get to moan about paradoxes. Google "Hurkens paradox" for the deal on how to do the bad.

@pigworker @julesh @JadeMasterMath genuine question: what's wrong with calling it Void?

@prophet @julesh @JadeMasterMath For centuries (in Computer Science years), C has used void to mean the unit type. Pretending that never happened is pure gaslight.