Here’s an idea for a type inference algorithm. For my project, I do not need an algorithm which determines types, just an algorithm which can answer questions about them. Also, I am not checking types; the fundamental assumption of my language is that the programmer is always right. I am simply getting as much information as I can in order to help understand what the programmer meant.
This is a form of polymorphism which, instead of generalizing during unification just carries around its constraints. It is a sort of let-polymorphism which works on all lambda abstractions. I’ll show by example. Consider the Haskell expression (f -> (f 0, f "")) id. Haskell rejects this program as ill-typed, but it clearly makes sense. So let’s try to make sense of it.
We want to type infer the expression: (λf -> (f 0, f "")) id -- Give types to the subexpressions of the lambda f :: a f 0 :: b f "" :: c (f 0, f "") :: (b,c) -- Find constraints a <: Int -> b -- from the application f 0 a <: Str -> c -- from the application f "" -- Generalize to lambda (bind all free variables under forall) -- The | is to be read "as long as" λf -> (f 0, f "") :: forall a b c. a -> (b,c) | a <: Int -> b ; a <: Str -> c -- This is the type of id (a builtin, so we knew that) id :: forall d. d -> d (λf -> (f 0, f "")) id -- Instantiate the lambda, substituting the type of id for a :: forall b c. (b,c) | (forall d. d -> d) <: Int -> b ; (forall d. d -> d) <: Str -> c -- Expand the equations into dependent sets :: forall b c. (b,c) | (exists d. Int <: d ; d <: b) ; (exists d. Str <: d ; d <: c) -- Reduce constraints :: forall b c. (b,c) | Int <: b ; Str <: c -- Constraint specification :: (Int, Str)
It looks pretty and powerful. After playing with this system a little bit, I discovered exactly how powerful it is. When you start putting constrained types into constraints, it becomes clear that you are embedding all of first-order logic. (For those who aren’t familiar with this kind of thing, the most common problem with type systems is that they are too powerful, not not powerful enough: once you can embed PA, it is possible to write a program that will never finish compiling!).