Lambda the Ultimate

In the thread on value level programming we started discussing an HM (like) type system with principal typings. Although based on Olaf Chitil and Grego Erdi's work, it seems what I have implemented has significant differences. There is also some influence from Kfoury and Well's System-I and System-E.

Key differences: There is no type environment (as it is compositional), and the typing context is a multi-set instead of a set. This seems equivalent to allowing rank-1 intersection types in the context, but by keeping the types themselves free of intersection operators, a normal HM unification operation can be used, which is decidable.

A few key claims: It is decidable, compositional, and has principal typings.

- I would like comments on the notation for the formal description of the type system, can it be improved?

- I tend to assume everything has been done before, but looking back this seems more original than I thought? Has anyone seen this before or can I count this as its first publication?

As the multi-set context effectively allows rank-1 intersections in the context, but not in the types themselves, a rank-0 intersection type seems a good term for this.

So here's my first attempt at writing the rules:

Rank 0 Intersection Type System Definition:

------------- LIT
{} |- N : Int


---------------- VAR
{x : a} |- x : a

where
    new a


M1 |- E1 : t1    M2 |- E2 : t2
------------------------------ APP
       M |- E1 E2 : t

where
    new a
    SUBS = t1 unify (t2 -> a)
    M = SUBS(M1 multi-set-union M2)
    t = SUBS(a)


 M1 |- E1 : t1
---------------- ABS
M |- \x . E1 : t

where
    new a
    SUBS = empty-substitution-list
    for t' in M1(x):
        SUBS = SUBS append (SUBS(a) unify SUBS(t'))
    M = SUBS(M1 - x)
    t = SUBS(a -> t1)


M1 |- E1 : t1      M2 |- E2 : t2
-------------------------------- LET
   M |- let x = E1 in E2 : t

where
    SUBS = emtpy-substitution-list
    M' = M2 - x
    for t' in M2(x):
        (M1' t1') = SUBS(M1 t1) with fresh free variables
        SUBS = SUBS append (SUBS(t') unify t1')
        M' = M' multi-set-union M1'
    M = SUBS(M')
    t = SUBS(t2)