User loginNavigation 
On Presenting the Semantics of Cat FormallyFirst 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://lambdatheultimate.org/node/1879 and http://lambdatheultimate.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 OperationsThe 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)  (TEVAL) T : [p] eval : (r A)>(r B) T : p : (r A)>(r B)  (TDIP) T : [p] dip : (r A 'c)>(r B 'c) T : p : (r A)>(r B)  (TDIIP) 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  TDIP [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!By cdiggins at 20070112 01:42  LtU Forum  previous forum topic  next forum topic  other blogs  5381 reads

Browse archivesActive forum topics 
Recent comments
11 hours 21 min ago
11 hours 39 min ago
11 hours 43 min ago
2 days 8 hours ago
2 days 17 hours ago
3 days 37 min ago
3 days 1 hour ago
3 days 8 hours ago
3 days 9 hours ago
3 days 11 hours ago