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

Browse archivesActive forum topics 
Recent comments
3 days 21 hours ago
4 days 16 hours ago
4 days 20 hours ago
4 days 20 hours ago
4 days 21 hours ago
4 days 22 hours ago
4 days 23 hours ago
4 days 23 hours ago
5 days 3 hours ago
5 days 3 hours ago