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.

I've been continually surprised by both the amount and the quality of comp sci literature that can be obtained from the web. Other than text books, there have been only a few occasions when I've been unable to locate an article. However one such exception has been Landin's "The Mechancial Evaluation of Expressions". At this point it feels that every other article I read cites Landin's paper. I have all of his other major papers, but TMEE is the one that is mentioned as the most central. I've tried and failed numerous times. Most inexplicably the Oxford Journal website appears to have no notion that this paper exists. Can anyone help me.

I've recently been toying with various approaches for supporting some level of intellisense on a dynamically typed language, specifically Lua (a functional scripting language with lexical scoping). I'd like to bounce some ideas around the community and hear some opinions. I should pretext this by stating that I'm not really a "languages guy." I have a CS degree with the standard compilers course but no advanced experience...which is probably why I was naive enough to undertake this in the first place :P But I have a significant amount working.

Since intellisense information is based on type information, there are inherent difficulties in implementing this for dynamic languages. The problem I'm most interested in is the following.

Let's say we have a name n in the scope s which is assigned different types within a conditional statement. For example, assume N and M are valid variables with different types below.

function s()
local n

if x then n = N else n = M end

...
end

We want to be able to resolve the type of n to provide intellisense information for it after the assignment. In order to do so, it seems we must first resolve x. However, this may not be possible outside of runtime (it could be a runtime lib call for instance). A similar problem occurs when a function has multiple return statements.

The solution I'm currently considering is to present all possibilities to the user. For instance, in the example above we know n is either type of N or type of M. In an environment like Visual Studio or Eclipse the intellisense drop down could display both possibilities with a special icon or text that indicates the ambiguity. In some situations, it may be obvious to the author what the correct option is for a given case. In a nutshell, if the parser can't figure it out statically then we ask the author to disambiguate and treat the name as the disambiguated type from that point forward. At least until it's made ambiguous again by a similar sort of assignment.

I can see a somewhat controversial aspect of this being that it can make you think about types while coding in a dynamically typed language. Also, since it's implied that the parser must keep track of every assignment, scalability is a concern.

Comments? Alternatives? Will this be useful?

Cheers,
Trystan