Tech Talk: The Little Typer With Daniel Friedman and David Thrane Christiansen
CoRecursive: Coding Stories
00:00
Type Theory - Can Types Refer to Theirself in This World?
Russell's type theory gets around this by saying that every set doesn't get to refer to things willy nilly. And then this paradox goes away, because it doesn't even make sense to ask the question of whether the set contains itself. So what we do in in pi is we have a type that describes most other types, but not itself, and also not types that contain itself. In typer ah industrial strength systems they all have infinitely many universe types where each of them talks about the ones that are smaller than itself. But nobody ever actually used anything more than one universe so we just rimmed the rest out.
Transcript
Play full episode
