New answers tagged type-theory
1
There is no assumption in your proof that the functions involved are computable, so it would be quite stingy to interpret the proof that way merely because Agda allows you to compute with its terms.
Rather, yes how it should be interpreted depends on the model, and constructive (in the sense of just removing axioms) proofs like the one you've given enable an ...
2
Structural type systems don't necessarily have anything to do with records. For instance, you could have a system where:
data Bool = False | True
data Two = Zero | One
are actually the same type, because they are both types with two nullary constructors. It also doesn't necessarily tell you much about records, because even though types are determined by ...
4
So, the answer is arguably "yes," this is an example of dependent types. However, the problem with a lot of simple examples that people create for this is that they don't demonstrate non-trivial aspects of dependent typing.
Arguably yours is better in this respect, because the type in question depends on an arbitrary value in MemorySlabCache. ...
5
Canonicity does not imply weak normalization. First, let me phrase the involved definitions more precisely:
WN: every open term is reducible to a normal term
Canonicity: every closed term is reducible to a canonical term
(Note: in modern metatheory of type theory, it is more common to talk about conversion instead of reduction, and likewise to talk about ...
Top 50 recent answers are included
