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