The Type of a Recursive Combinator

The latest Cat version ( 0.9.7 at ) now has a linear recursion combinator "rec". The Cat type inference algorithm currently can't handle self-referential functions, but you implement recursive algorithms using the rec combinator.

Here is an example of the factorial program:

  >> define f { [dup 1 <=] [*] [pop 1] [dup --] rec }
  inferred type for program 'f' as ( int ) -> ( int )
  main stack: _empty_
  >> 5 f
  main stack: 120
  >> 6 f
  main stack: 120 720

The type of the rec combinator is interesting (at least I thought so):

  (A:any*)->(A A) // argument relation
  (A)->(B:any*)   // termination function
  (A B)->(B)      // result relation
  (A)->(bool A)   // termination condition
  A               // input 

I was wondering what people's thoughts were about the rec combinator? For example is it in fact interesting or novel to see the types explicitly stated for each component of linear recursion? Do you think there might be some educational value for students to have recursion explained in terms of arguments to a combinator?

Any feedback would be very helpful, thanks in advance!

Note: those familiar with Cat will notice that stack descriptions now read left to right, where the leftmost type corresponds to the top of the stack.

Comment viewing options

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

This is a pure guess, but

This is a pure guess, but what if you transform all recursive functions into identical functions that use the Y combinator (only for the purpose of type inference not necessarily the actual impl.) and use the type of the transformed function as the type of the recursive function.

Good idea

This sounds like a very interesting and promising idea. I haven't implemented a Y combinator yet but I am going to look into this. Thanks for sharing the idea with me.