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. 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
- (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”.
 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 :-).