Singleton Types are the Key to Co-dependency

Since the last time I wrote about existentials I had a plenty of time to ponder how they fit into the qualifier-typed typed lambda calculus which de Bruijn has proposed, and I am very proud of implementing a formalization for.

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:

1. the treatment of patterns that are values was missing,
2. the handwavy argument how the proposition corresponding to the condition is encoded,
3. that the dependent sum binder introduced two variables (where lambdas only introduce one),
4. and finally that parenthesized condition after the ∃-quantor which do not seem to appear in logic textbooks.

It was the first worry that kept me awake this night. Here is a prototypic definition:

fac 0 = 1

fac (1+n) = (1+n) * fac n

In Dylan (an object-oriented functional language) one would write the first branch of same function as

define method fac (n :: singleton(0)) 1 end

Here 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 . x

where 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)〉 . y

here 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.