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

Browse archives
Active forum topicsNew forum topics 
Recent comments
11 hours 21 min ago
15 hours 16 min ago
1 day 2 hours ago
1 week 5 days ago
1 week 5 days ago
3 weeks 3 days ago
6 weeks 5 days ago
6 weeks 6 days ago
6 weeks 6 days ago
7 weeks 1 day ago