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.
@pigworker I've been wanting to track down for some time where "void" as a type name originated and what its original meaning was (and whether a later language borrowed it from an earlier one and changed it); if you have any leads they would be much appreciated. Apparently you reckon C had it first?
@pigworker I hadn't contemplated that *that* Data.Void proposal might've been *the* Haskell-side origin (having assumed it to be more ancient); looking back at that discussion though, there is a message from Lennart that it was, in fact, already in 1.4: https://mail.haskell.org/pipermail/libraries/2006-October/005991.html
And checking just now, it seems to have also been in 1.3, but not, seemingly, 1.2. So, that's at least one question answered.