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

[Daniel Fischer]

Am Freitag, 4. März 2005 19:35 schrieb 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?

If I remember correctly, an "occurs check" is checking whether a type variable 
(call it 't') occurs as an argument to a tuple constructor or function arrow 
in a type expression to be substituted for t, as above or in 
t = t -> t1.

Such occurences would lead to an infinite type, hence are forbidden.
If you really think you need such things, 

data Pair a b = P (a, (Pair a b))

works, however that type contains no fully defined values, so is only of 
limited usefulness.

I have a fix for the factorial and similar recursive functions, though it's 
not really easy (and needs extensions):
don't define the recursion combinators via Stack, do it like this:

linrec2 :: forall a. (forall b. (a,(a,b)) -> (a,b)) ->
                     (forall b. (a,b) -> (a,(a,b))) ->
		     (forall b. (a,b) -> (a,b)) ->
		     (forall b. (a,b) -> (Bool,b)) ->
		     (forall b. (a,b) -> (a,b))
linrec2 rec2 rec1 t p stack
   | fst $ p stack = t stack
   | otherwise = rec2 $ linrec2 rec2 rec1 t p (rec1 stack)

and similarly for genrec. Then you can define

fact6 = linrec2 mult (dup ! pre) suc nul.

You cannot use linrec, because rec2 and rec1 must each have identical result 
and argument types:
*Joy> :t linrec
linrec :: forall t b b.
          (t -> t, (b -> b, (b -> t, (b -> (Bool, b), b)))) -> t

I don't know Joy, but probably there the stack is (roughly) a heterogenous 
list, which is hard to model in Haskell, think of

data Element = Bool Bool
                      | Char Char
                      | Int Int
                       . . .
                      | IntToBool (Int -> Bool)
                       . . .

type Stack = [Element]

and how to define functions for that, urgh.
>
>
> 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)
                             ^^^^^^^^^^
             fst (p stack) suffices.

> >      | 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
>
Hope, I could help a little,
Daniel