Home » forums » LtU Forum

Modeling and Typing Combinatory Calculus

I 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
argument, while K2 is only partially evaluated if given one parameter.

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

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

How would you type S ?

I can't immediately see a type for the S combinator that would work with ('a 'b -> 'a) for the K combinator. Maybe I'm missing something there, but I'd suggest the obvious approach of typing S and K in the curried lamba calculus style ('a -> ('b -> 'a))

So long as you choose the types of K and S to be consistent with eachother, though, I don't see a problem. You just want a consistent embedding of the simply typed lambda calculus into your language and its type system, right?

By Matthew Willson at Fri, 2006-12-22 19:31 | login or register to post comments

I can't immediately see a

I can't immediately see a type for the S combinator that would work with ('a 'b -> 'a) for the K combinator.

I believe it would look like (I haven't yet worked this out formally though):

S : ('a) ('a -> 'b) ((('a -> 'b) 'a) -> 'c) -> ('c)

I have to confess I don't like this much because it strays so far from the traditional typed lambda calculus. However AFAICT this appears to correctly describe the types of the applicative combinators used in Brent Kerby's paper The Theory of Concatenative Combinators

Maybe I'm missing something there, but I'd suggest the obvious approach of typing S and K in the curried lamba calculus style ('a -> ('b -> 'a))

It pays to be obvious I suppose. :-)

So long as you choose the types of K and S to be consistent with eachother, though, I don't see a problem.

This is what my intuition is telling me as well.

You just want a consistent embedding of the simply typed lambda calculus into your language and its type system, right?

Yes, I figure this would be a good way to demonstrate the completeness of the type system. I see that a lot of programming language papers relate their type system to the typed lambda calculus (or some derivative), so I figure mapping to and from the typed SK calculus would be a useful exercise for a paper introducing a new programming language. I would appreciate hearing other people's opinions on the subject though.

Thanks for your feedback!

By cdiggins at Fri, 2006-12-22 21:01 | login or register to post comments