The headline has already spoiled the suspense, but the interesting part is how I arrived at that assertion. It happened last night and it carries all the attributes of an epiphany :-)
There were some anomalies that worried me about the introduction of existential qualifiers in the prequel post:
- the treatment of patterns that are values was missing,
- the handwavy argument how the proposition corresponding to the condition is encoded,
- that the dependent sum binder introduced two variables (where lambdas only introduce one),
- and finally that parenthesized condition after the ∃-quantor which do not seem to appear in logic textbooks.
fac 0 = 1
fac (1+n) = (1+n) * fac nIn Dylan (an object-oriented functional language) one would write the first branch of same function as
define method fac (n :: singleton(0)) 1 endHere the singleton function returns a type whose sole inhabitant is the argument to singleton. This analogy pushed me over the top. What if I introduced the concept of co-dependency in my formalization? Say,
∃x:singleton 1 . xwhere values can be lifted up in the type realm and appear at the right-hand-side of the type judgement (:). I prefer to call this co-dependency because it is opposite to regular dependency which happens in the returned expression. Consider the following type-theory expression:
λx:Int . 〈y:singleton (5*x)〉 . yhere a universally quantified variable (x) is entering an expression which is the argument to the singleton construct giving the type to y. What does it mean? That for every x there is an y of 5 times the magnitude, which becomes the result.
With this interpretation all my worries have vanished: there is just one variable added by the dependent sum quantification and the condition is now neatly tucked away on the right side of the colon!
Next to come: introduce this idea into the formalization.