Tuesday, December 14, 2010

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.

6 comments:

beroal said...

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.
Can you please point to a specific page in that article that has the phrase "qualifier-typed typed lambda calculus"?

heisenbug said...

@beroal: De Bruijn uses the term "lambda-typed lambda calculus" (in the title). I did two deliberate changes to this term:
1) 'lambda-typed' -> 'qualifier-typed', because in mid-term I intend to support the sigma family, i.e. dependent sums, too (not sure de Bruijn considered these). 'Lambda', at least to me, has the dependent product association.
2) I added 'typed' because additionally to the strata and 'degree' (as de Bruijn calls them) I wish to precisely encode the types of terms (such as 42::Int), etc. I do not see yet how this falls out of the paper (I guess he is employing the church encoding of data types).

heisenbug said...

@self: s/qualifier/quantifier/g
:-( sorry for the confusion...

winterkoninkje said...

"co-dependency" is a bad name. There are two different things going on in dependent types: first is the ability to lift values into the type level, second is the ability to introduce dependencies between function arguments and their return values (or between the first half of a tuple and the second half). You can have the former without the latter, and many languages which don't support full dependent types do this. That's all you have there in the existential. The quantificand doesn't depend on anything, it just has a value in its type is all.

Dan Licata said...

These kinds of issues come up frequently in work on the ML module system, where dependent pairs are used to represent modules and singletons are used to represent type definitions. For example:

Extensional Equivalence and Singleton Types.
Chris Stone and Robert Harper.
http://www.cs.cmu.edu/~rwh/papers/singletons/tocl.pdf

beroal said...

In Dylan (an object-oriented functional language)… Here the singleton function returns a type whose sole inhabitant is the argument to singleton.

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


After pondering on articles and source codes you referenced I must admit I am defeated. I just can not understand how can you mix all of this. :) Dylan (the programming language) has dynamic typing. You seem to use intuitionistic type theory (ITT) (or calculus of inductive constructions, Barendregt's lambda cube, Coq, Agda etc.). IMHO intuitionistic type theory is related to Dylan in no way. No OOP style subtyping. No "type which only inhabitant is a particular number". However, ITT has numbers at the right side of ":". There you also can construct an analogue of your singleton, i.e. an unary predicate which is true only on a single number.

The paper by Steven Awodey particularly bewildered me, as it is about ITT in homotopy theory. O_O