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

Browse archivesActive forum topics 
Recent comments
22 hours 4 min ago
23 hours 9 min ago
1 day 36 min ago
1 day 7 hours ago
1 day 11 hours ago
1 day 15 hours ago
1 day 15 hours ago
1 day 15 hours ago
1 day 17 hours ago
1 day 17 hours ago