39 ms·
I'm no type theory expert, but if you can describe natural numbers as: Even (n: Natural) | n % 2 == 0 Then what's stopping you from doing: Undecidabl
by slightknack 6y ago
I'm no type theory expert, but if you can describe natural numbers as:
Even (n: Natural) | n % 2 == 0
Then what's stopping you from doing:
Undecidable _ | loop {}
I'm not sure, but I think that's because strict dependent language systems like Pie (similar to CoC) use induction over the structure of a type for decidability. If I had 'the little typer' on hand, I'd elaborate more on this point. I think there's some relation between undecidability and the type Absurd, but I'd have to look into it more.
- slightknack 6y agoOh, I think I just confused refinement types with dependent types. The above still stands though.
- ojnabieoot 6y agoJust FYI, most dependent type systems don’t typecheck when a parameter to a type constructor is a function, since they can’t “deduce” very much about a function except its signature. They can take proof objects (including objects involving evaluated functions, like ‘n % 2 = 0’) but not functions by themselves (like ‘loop {}’). This isn’t a technical problem with unification, the issue is a fundamental conflict between “intensional” versus “extensional” equality. Wikipedia has a good example that communicates the underlying confusion: https://en.wikipedia.org/wiki/Extensionality https://en.wikipedia.org/wiki/Extensionality AFAIK all depedently-typed general-purpose languages use intensional equality since it’s consistent, but there are proof-checkers that use extensional dependent type theories (inconsistency is less of a problem than you might think, and actually makes some higher-order topology and set theory much easier to program).