4 ms·
I'm not an expert on type theory, but I would guess "Turing complete types" make type checking an undecidable problem, similar to how dependent types make type
by koito17 3y ago
I'm not an expert on type theory, but I would guess "Turing complete types" make type checking an undecidable problem, similar to how dependent types make type inference undecidable, since dependent types let you more or less encode arbitrary things into a type (e.g. p is a value of type Prime). That at the very least gives you an infinite search space, and the possibility to encode e.g. a halting property into types.