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.

Thanks in advance!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

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


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.