[Haskell-cafe] Joy Combinators (Occurs check: infinite type)

[Greg Buchholz]

    Recently, while investigating the (non-statically typed) stack-based
functional language Joy (http://www.latrobe.edu.au/philosophy/phimvt/joy.html),
I became interested in seeing if I could implement Joy's combinators in 
Haskell.  I started with a stack based implementation using nested
tuples as the stack.  Things worked out well until I got to the
recursion combinators.  Even then, things didn't seem that bad, since
Haskell was able to infer types for the the linrec and genrec
combinators.  Trouble popped up when I tried to apply the recursion
operators to a function (in this case calculating the humble factorial).
In the code below, fact3,4 & 5 all fail with an "Occurs check" that
looks something like the following...

joy3.hs:24:
    Occurs check: cannot construct the infinite type: t = (a, t)
        Expected type: ((a5 -> (a, (a, t)), a5) -> (a, t),
                        ((a1, t3) -> (a1, (a1, t3)),
                         ((a2, t2) -> (a2, t2), ((a3, t1) -> (Bool, t1),a4))))
                       -> c
        Inferred type: ((a5 -> (a, (a, t)), a5) -> (a, (a, t)),
                        (a5 -> a5, (a5 -> (a, (a, t)), (a5 -> (Bool, b),a5))))
                       -> (a, (a, t))

...Normally, I would have given up and declared that Joy wasn't an easily
typed language, but I'm motivated to dig further because if you remove
the type signature from "fact" below, it also fails with an "Occurs
check".  So, can anyone direct me towards more information on exactly
what an "Occurs check" is, or does anyone see an easy fix to my
problems?


Thanks,

Greg Buchholz 

P.S. The first thing you should note about the code below is the
definition of the reverse composition operator (!), which I used to give
the program a more Joy-like feel. (i.e. (!) f g = g.f)

>--Joy combinators in Haskell
>
>main = do   print $ ((lit 6) ! fact) bot            -- factorial of 6
>            print $ ((lit 2) ! square ! fact2) bot  -- factorial of 4
>
>bot = "EOS" -- end of stack
>square = dup ! mult
>cube = dup ! dup ! mult ! mult
>
>--In Joy: factorial == [0 =] [pop 1] [dup 1 - factorial *] ifte
>fact :: (Integer, a) -> (Integer, a)
>fact =  (quote ((lit 0) ! eq)) !
>        (quote (pop ! (lit 1))) !
>        (quote (dup ! (lit 1) ! sub ! fact ! mult)) !
>        ifte
>
>--In Joy: [1 1] dip [dup [*] dip succ] times pop
>fact2 = (quote ((lit 1) ! (lit 1)))
>        ! dip ! (quote (dup ! (quote mult) ! dip ! suc))
>        ! times ! pop
>
>{- fact3,4 & 5 don't type check, fails with...
>-- Occurs check: cannot construct the infinite type:
>
>--In Joy: [null] [succ] [dup pred] [i *] genrec
>fact3 :: (Integer, a) -> (Integer, a)
>fact3 = (quote nul) ! (quote suc) ! (quote (dup ! pre)) ! (quote (i ! mult))
>        ! genrec
>
>fact4 :: (Integer, a) -> (Integer, a)
>fact4 = genrec.quote(mult.i).quote(pre.dup).quote(suc).quote(nul)
>
>--In Joy:  [null]  [succ]  [dup pred]  [*]  linrec
>fact5 :: (Integer, a) -> (Integer, a)
>fact5 = quote(nul) ! quote(suc) ! quote(dup ! pre) ! quote(mult) ! linrec
>
>--}
>nul = (lit 0) ! eq
>suc = (lit 1) ! add
>pre = (lit 1) ! sub
>
>linrec (rec2, (rec1, (t, (p, stack))))
>      | fst (p stack) == True = (t stack)
>      | otherwise = rec2 (linrec (rec2, (rec1, (t, (p, (rec1 stack))))))
>
>genrec (rec2, (rec1, (t, (b, stack))))
>      | fst (b stack) == True = (t stack)
>      | otherwise = (rec2.quote(genrec.quote(rec2).quote(rec1).
>                          quote(t).quote(b))) (rec1 stack)
>
>times (p, (n, stack)) | n>0 = times (p, (n-1, (p stack)))
>                      | otherwise = stack
>
>(!) f g = g.f
>i    (a, b)      = (a b)
>add  (a, (b, c)) = (b+a, c)
>sub  (a, (b, c)) = (b-a, c)
>mult (a, (b, c)) = (b*a, c)
>swap (a, (b, c)) = (b, (a, c))
>pop  (a, b)      =  b
>dup  (a, b)      = (a, (a, b))
>dip  (a, (b, c)) = (b, (a  c))
>eq   (a, (b, c)) | a == b    = (True, c)
>                 | otherwise = (False,c)
>
>ifte (f, (t, (b, stack))) | fst (b stack) == True = (t stack)
>                          | otherwise             = (f stack)
>
>lit val stack      = (val, stack) -- push literals on the stack
>quote = lit
>