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 stack-based 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 2006-12-20 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