Proof irrelevance has been removed to solve an issue with projections, but it is being added back with another technique, which should be much simpler. Previously, I've been synthesizing the types of value at conversion check, so that at each recursion step we could check whether the type was a prop or a unit-like type.
This seemed to me at first to be better than Lean's approach of inferring the type of the values at each recursion step, since inference is a slow process. Lean has a infer cache, which could make the inference return in O(1) time, but since the reducing of expressions creates expressions on the fly, I thought this would create new hashes and thus there would be cache misses. Though after some thought, I've realized you could export the hash of the app node in a beta redex to the newly created node after beta reduction, since types are preserved by beta reduction.
This gave me the idea of annotating expressions and values through a new enum field, denoting whether the expression or value is a Prop, Unit, proof, or value of a Unit type, since this is the only information we need to extract from the inferred type. This field will be populated while typechecking expressions, and will be preserved in reduction because of the type preservation property of beta reduction. I believe this is a better approach than using caches, since matching enum values is way faster than retrieving a cached value and inspecting it, which must be done at every recursion step of the conversion checker, which could potentially be tens of millions of times
Proof irrelevance has been removed to solve an issue with projections, but it is being added back with another technique, which should be much simpler. Previously, I've been synthesizing the types of value at conversion check, so that at each recursion step we could check whether the type was a prop or a unit-like type.
This seemed to me at first to be better than Lean's approach of inferring the type of the values at each recursion step, since inference is a slow process. Lean has a infer cache, which could make the inference return in O(1) time, but since the reducing of expressions creates expressions on the fly, I thought this would create new hashes and thus there would be cache misses. Though after some thought, I've realized you could export the hash of the app node in a beta redex to the newly created node after beta reduction, since types are preserved by beta reduction.
This gave me the idea of annotating expressions and values through a new enum field, denoting whether the expression or value is a
Prop,Unit, proof, or value of aUnittype, since this is the only information we need to extract from the inferred type. This field will be populated while typechecking expressions, and will be preserved in reduction because of the type preservation property of beta reduction. I believe this is a better approach than using caches, since matching enum values is way faster than retrieving a cached value and inspecting it, which must be done at every recursion step of the conversion checker, which could potentially be tens of millions of times