Lambda Constraint Typing

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!).


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s