User loginNavigation 
Modeling and Typing Combinatory CalculusI am working on modeling the typed SK calculus in Cat, and I have reached an impasse. I believe it is well established that the type of the K combinator in most functional languages can be expressed: K : 'a > 'b > 'a The dilemma I am facing is how I should model this in a typed stackbased language (or concatenative language if you prefer). I am wavering between two possibilities: K1 : ('a > ('b > 'a)) K2 : ('a 'b > 'a) So far it appears that both approaches are valid, they simply differ in whether the "function application" operation is implied in the K combinator or not. Allow me to demonstrate: 42 K1 : ( > ('a > 42)) 42 K2 : ('a > 42)
In plain english K1 will push a function onto the stack if given one Adding another argument illustrates the issue more clearly: x 42 K1 apply == 42 x 42 K2 == 42 The same problem can also be framed in terms of the I combinator: [f] I == [f]? [f] I == f? I was wondering if anyone has any insight into this problem that they could share? By cdiggins at 20061220 20:42  LtU Forum  previous forum topic  next forum topic  other blogs  6326 reads

Browse archives
Active forum topics 
Recent comments
21 weeks 17 hours ago
21 weeks 21 hours ago
21 weeks 21 hours ago
43 weeks 2 days ago
47 weeks 4 days ago
49 weeks 1 day ago
49 weeks 1 day ago
51 weeks 6 days ago
1 year 4 weeks ago
1 year 4 weeks ago