Lambda the Ultimate

First I want to say that I owe a debt of gratitude to the LtU community for the generous help I've had in developing the type system for Cat. Two threads last month were particularly helpful for me: http://lambda-the-ultimate.org/node/1879 and http://lambda-the-ultimate.org/node/1899. So thank you very much to everyone who contributed to these threads (and previous ones as well).

I have been working hard on writing an article to present the Cat language formally, but I still lack confidence in my approach to presenting the type system. I felt that it would be useful in a paper which presents the semantics of Cat to demonstrate an implementation of the typed SK calculus. One burning question I have is whether such an endeavour would add value to the paper?

Below is a synopsis of how I am planning on presenting the type system and SK calculus in the paper. For the purposes of this post I only show the type derivation of the K combinator, since the S combinator is much longer.

The r stands for the row variable (rho or ρ).

  pop : (r 'a -> r)
  dup : (r 'a -> r 'a 'a)
  swap : (r 'a 'b -> r 'b 'a)
  dip : (r 'a 'b ('a -> 'c) -> r 'c 'b)
  diip : (r 'a 'b 'c ('a -> 'd) -> r 'd 'b 'c) EDIT
  eval : (r 'A ('A -> 'B) -> r 'B)

These are attributed to Andreas Rossberg.

  -------------------------------------------- (EMPTY)
  T :- empty : (r)->(r)

  T(x) = forall a1..an A1..Am.t
  -------------------------------------------- (VAR)
  T :- x : t[t1/a1]..[tn/an][r1/A1]..[rm/Am]

  -------------------------------------------- (CONST)
  T :- c : (r)->(r prim)

  T :- p : t
  -------------------------------------------- (QUOTE)
  T :- [p] : (r)->(r t)

  T :- p1 : (r1)->(r2)    T :- p2 : (r2)->(r3)
  -------------------------------------------- (COMPOSE)
  T :- p1 p2 : (r1)->(r3)

  T :- p : (r A)->(r B)
  ---------------------------------------- (T-EVAL)
  T :- [p] eval : (r A)->(r B)

  T :- p : (r A)->(r B)
  ---------------------------------------- (T-DIP)
  T :- [p] dip : (r A 'c)->(r B 'c)

  T :- p : (r A)->(r B)
  ---------------------------------------- (T-DIIP)
  T :- [p] diip : (r A 'c 'd)->(r B 'c 'd)

K is implemented as "[pop] dip eval". The derivation is:

    pop : (r0 'a0 -> r0)
  0 ---------------------------------------------------- T-DIP
    [pop] dip : (r1 'a1 'b1 -> r1 'b1),
    eval : (r2 'A2 ('A2 -> 'B2) -> r2 'B2)
  1 ---------------------------------------------------- COMPOSE
    [pop] dip eval : (r1 'a1 'b1 -> r2 'B2)
    , r1 'b1 = r2 'A2 ('A2 -> 'B2)
    ,'b1 = ('A2 -> 'B2)
    , r1 = r2 'A2
  2 ---------------------------------------------------- UNIFY
    [pop] dip eval : (r2 'A2 'a1 ('A2 -> 'B2) -> r2 'B2)
  3 ---------------------------------------------------- SIMPLIFY
    [pop] dip eval : (r 'A 'b ('A -> 'C) -> r 'C)

What I am hoping for are suggestions on how I can better present the semantics of Cat in a way which would be appropriate for a "serious" paper, but also would make sense to relative newcomers to type theory.