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  5470 reads

Browse archives
Active forum topicsNew forum topics 
Recent comments
1 week 1 day ago
1 week 4 days ago
2 weeks 5 days ago
3 weeks 1 day ago
3 weeks 2 days ago
3 weeks 2 days ago
4 weeks 6 days ago
4 weeks 6 days ago
6 weeks 4 days ago
9 weeks 6 days ago