## On Presenting the Semantics of Cat Formally

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.

Types of Common Operations

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)
Core Typing Rules

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)
Supplemental Typing Rules
  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)
Derivation for the K Combinator

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.

## Comment viewing options

### Is 'diip' correct?

Above you have written:
 diip : (r 'a 'b 'c ('a -> 'd) -> r 'c 'd) 

And below you have written:
 T :- p : (r A)->(r B) ---------------------------------------- (T-DIIP) T :- [p] diip : (r A 'c 'd)->(r B 'c 'd) 

I'm not really sure I understand this, but it seems to me that diip is used above as, and would naturally be (at least if it is analagous to dip):
 diip : (r 'a 'b 'c ('a -> 'd) -> r 'd 'b 'c) 

Is this the correct definition?

Bryan Burgers

### Yes!

Thank you very much for catching this. I'm glad I was making enough sense, that you were able to catch this slip-up. :-)

### What is T-DIIP?

I thought maybe I should clarify. T-DIIP is a derived typing rule for applying the diip combinator to an arbitrary quotation.

Rather than deriving the type of an expression such as "[x] diip" from first principles (e.g. applying the "QUOTE" rule to, then applying the "COMPOSE" rule, then unifying) it is much simpler to simply apply the derived rule T-DIIP directly, saving a lot of virtual paper.

Whether this is a good approach or not is unclear to me, so I am inviting suggestions on how to improve my approach.