Re: [stack] disallowing recursive definitions

On Thu, Feb 28, 2008 at 9:19 PM, John Nowak <[email protected]> wrote:
>
>
> 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,

Cat does.

> which very well could be by your type checker is returning
> nonsense. (Of course, it's hard to tell for sure from here.)

I suspect this is the problem. Here is the fibonacci function again
(forcing it to use ints):

>> define fib { \f.\n.[n 1 lteq_int [1] [f n 1 sub_int f apply f n 2
sub_int f apply add_int] if] }

Here is the type:

fib : ( -> (A int int int int (A int int int int (A int int int int (A int int i
nt int ((B -> C) -> A int int int int) int -> A int int int int) int -> A int in
t int int) int -> A int int int int) int -> A int int int))

Looks like I am going to have reintroduce recursive types.

- Christopher