Re: [stack] disallowing recursive definitions

On Feb 28, 2008, at 5:23 PM, Christopher Diggins wrote:

> Incidentally this managed to completely corrupt my type checker,  
> thanks a lot!

I'd be surprised if Cat were able to handle such a translation in the  
general case. Take something like the ackermann function in Haskell:

    ack 0 n = n + 1
    ack m 0 = ack (m - 1) 1
    ack m n = ack (m - 1) (ack m (n - 1))

By passing the function itself as an additional argument, we can  
remove the recursive call:

    ackcore f 0 n = n + 1
    ackcore f m 0 = f f (m - 1) 1
    ackcore f m n = f f (m - 1) (f f m (n - 1))

    ack m n = ackcore ackcore m n

Unfortunately, this will fail the occurs check. The only way that Cat  
could not run into this problem is if it discards the recursive  
constraint, which very well could be by your type checker is returning  
nonsense. (Of course, it's hard to tell for sure from here.)

- John