I have been working on a type system for the last couple days, in case you haven’t noticed. But now I have one concrete and axiomatized, which is strong enough to infer the type of `(f -> f 0) id`. “Oh boy,” you might say, “what an accomplishment”. However, the generality of the system makes it seem like it can check many, if not all, other types. I just don’t know whether it’s decidable (but at least now that it is axiomatized, I can start to analyze it formally). And again, I don’t care if it’s decidable, as long as I can get an algorithm that gets it right “most of the time”.

Haskell types the identity function as `id :: forall a. a -> a`. That is to say, there is one identity function for every type `a`, and it has type `a -> a`. But arguments to functions must be “monomorphic”; that is, when you pass something which has a whole set of values or types, Haskell has to pick one before passing. That’s the reason `(f -> (f 42, f "hello")) id` does not compile: because `f` has type `a -> a` for *some* type `a`, not for every type (it has to be a specific function, not a whole class of them). `id` is perfectly capable of working on both integers and strings, so it is safe to pass its polymorphic form as `f`, but it is not well typed.

This type system is different: the type `forall a. a -> a` is a *single* type. In fact, nothing is typed with a whole set of types; every value that could be thus typed in Haskell has a single, unique type in this type system. This is done by defining the type of `forall a. a -> a` to be the least upper bound of the set of all types of that form.

A little type theory background: There is a type `Top` which is a supertype of every type (i.e. it admits any value), and there is a type `Bot` which is a subtype of every type (i.e. it admits no values).

Here are my axioms. The non-logical symbols are (<:) for “subtype” and A(x,y) for the arrow type “x -> y”.

- ∀ a ∀ b ∀ c ((a <: b ∧ b <: c) ⇒ a <: c)
- ∀ a ∀ b ((a <: b ∧ b <: a) ⇔ a = b)
- ∀ a ∀ b ∀ c ∀ d (A(a,b) <: A(c,d) ⇔ (c <: a ∧ b <: d))
*for each atomic type A in the calculus:*∀ a ∀ b (A ≠ A(a,b))*Schema: for each wff φ(x):*∃ a such that the following hold:- ∀ x (φ(x) ⇒ x <: a)
- ∀ x (∀ y (φ(y) ⇒ y <: x) ⇒ a <: x)
- ∀ x (x <: a ⇒ (x = a ∨ ∃ y (x <: y ∧ φ(y))))

And here is an explanation of each of the axioms:

Axioms 1 and 2 simply state that the subtype relation is a partial order; i.e. that if, say, Even is a subtype of Int and Int is a subtype of Num, then Even must be a subtype of Num. It also says that if you can sandwich a type between another type and itself, the two must be equal; i.e. if Int is a subtype of Foo and Foo is a subtype of Int, then Foo and Int must actually be the same type.

Axiom 3 defines what it means for two functions to be subtypes of each other. A function g is a subtype of a function f just in case f is “more accepting” and “less giving” than g. That is, if anything you can give to g you can give to f, and anything you can expect from f you can expect from g.

Axiom 4 says that there are types which are not functions[1]. This will depend on the particular incarnation of the type system. You might have Int, String, Num, Bool, etc. For now, we will consider the system with only one such atomic type: Int.

Axiom 5 is the big one. It says that every set of types has a least upper bound, and that said upper bound includes nothing more than the types in the set and their subtypes. More verbosely: 5.1 says that there is an *a* which is an upper bound, 5.2 says that *a* is the *least* upper bound (any other upper bound is a supertype of *a*), and 5.3 says that any subtype of *a* has to be either *a* itself or a subtype of one of the things in the set. This is the axiom which allows us to consider the type `forall a. a -> a` a single type, rather than a set of types. It’s simply the least upper bound of the corresponding set.

So, let’s find out the type of `(f -> f 0) id`. Let’s define `l = (f -> f 0)`, and say that `l`‘s type is L, `id`‘s type is ID, and `l id`‘s type as R (for result). L is least upper bound (lub) of `forall a. (Int -> a) > a`, ID is the lub of `forall a. a -> a`. We will define the type of the application `l id` as ∀ x (A(ID,x) <: L ⇔ x <: R). I claim that R is the type `Int`. In order to show this, we will need a few lemmas:

**Lemma 1:** *a <: b if and only if ∀ x (x <: a ⇒ x <: b)*

Proof:(pretty trivial, but I’ll do it anyway)

- (⇒) Contrapositive: suppose there is some x with x <: a but not x <: b. Then if a <: b then x <:a <: b, so it must not be the case that a <: b.
- (⇐) Let x = a. Then a <: a by definition, so a <: b.

**Lemma 2:** *ID is not an arrow type*

Proof:Suppose it were: i.e. ID = A(a,b). Since it is an upper bound for all types of the form A(x,x), A(Bot,Bot) <: ID and A(Top,Top) <: ID. By axiom (3), a <: Bot and Top <: b. Of course, the only way that can happen (by definition of Bot and Top) is if a = Bot and b = Top. So ID = A(Bot,Top). Notice that, say, A(Int,Top) <: ID. By axiom (5.3), there must be some y such that A(Int,Top) <: A(y,y) (since A(Int,Top) ≠ A(Bot,Top)). Thus, by axiom (3) again, Top <: y and y <: Int. By axiom (1), Top <: Int, a contradiction!

**Lemma 3:** *If A(x,y) <: ID, then y <: x*

Proof:Suppose A(x,y) <: ID. Then by axiom (5.3), either A(x,y) = ID or there exists a z with A(x,y) <: A(z,z). We know by Lemma 2 that ID is not an arrow type, so ID ≠ A(x,y). So there is some z with A(x,y) <: A(z,z). Therefore by axiom (3), y <: z and z <: x, so y <: x by axiom (1).

**Theorem:** *R = Int*

Proof:

- (Int <: R) By the definition of R (stated just before the axioms), it suffices to show that A(ID, Int) <: L. Notice that by axioms (5.1), (3), and the definition of ID we have A(ID, Int) <: A(A(Int,Int), Int). Then by (5.1) and the definition of L we have A(A(Int,Int),Int) <: L. Therefore A(ID, Int) <: L.
- (R <: Int) By Lemma 1, it suffices to show that given x, x <: R implies x <: Int. Suppose x <: R. By the definition of R, A(ID,x) <: L. L is not an arrow type, so there is a y such that A(ID,x) <: A(A(Int,y),y) by axiom (5.3). Expanding by axiom (3), A(Int,y) <: ID and x <: y. By Lemma 3, y <: Int. But x <: y, so by axiom (1), x <: Int.

Now, even though interesting things can be done with this, it’s probably clear that this system isn’t necessarily decidable. I did get the computer (Prover9) to prove this, but only after telling it to prove those three lemmas first plus one more, and after that it cranked for about 45 minutes and then spat out a 93-line proof. Doing this automatically for a programming language isn’t practical as it stands. However, that’s not to say I couldn’t prove some more stuff and simmer this down into a nice algorithm, which is exactly what I intend to do. The power of this system suggests that it is undecidable, considering that it probably subsumes F_{<:}. But we at least have a basis for computation with this system, because we can store any type and use it without “type instantiation”.

[1] Incidentally, this is not true in the pure lambda calculus; everything is a function. This can cause quite a different incarnation of this type system. Since axiom 4 is the only axiom that requires any two things to be different, the pure lambda calculus admits a model of just one element: all things have the same type, namely “thing”. This is the untyped lambda calculus :-).

Hmm, it looks like this is just a complete semilattice with the arrow function and axiom 3. So I should learn some lattice theory and then look at the consequences of axiom 3 in-depth. However, I am considering adding an induction axiom; i.e. if you prove something for all the atomic types, then prove that if it holds for a and b it holds for A(a,b), then prove that if it holds for a set of types it holds for their least upper bound, then you have shown that it holds for all types. This sounds complicated, but it essentially says that all types are either atomic, finite arrows, or least upper bounds, nailing down the structure of the model that implements this theory.

Adding such an axiom would make this theory’s undecidability blatantly obvious: embed PA by mapping 0 to one of the atomic types and S(x) to A(x,x). At first I thought that this meant that the theory shown in the article was also undecidable, but I realize that that’s not necessarily true. If the induction axiom were called φ, and the undecidable sentence were called ψ, then obviously φ ⇒ ψ is undecidable in this theory. However, φ is not a single sentence, it is a schema, so φ ⇒ ψ is not a sentence because it is infinitely long.

But my hunch is that it’s still undecidable. One way to show that a theory is decidable is to show that all countable models are isomorphic, and I can show that this theory has two nonisomorphic countable models. However, these two models are still elementarily equivalent (one is just a “nonstandard model” of the other), so that still doesn’t imply incompleteness. Hmm, this comment is getting long. Maybe I should make it into a post.

This investigation sure is putting my math knowledge to the test, and teaching me a bunch more.