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

Browse archivesActive forum topics 
Recent comments
1 week 2 days ago
5 weeks 3 days ago
6 weeks 16 hours ago
6 weeks 16 hours ago
8 weeks 7 hours ago
8 weeks 7 hours ago
8 weeks 3 days ago
8 weeks 3 days ago
9 weeks 2 days ago
10 weeks 2 days ago