[Haskell-cafe] Joy Combinators (Occurs check: infinite type)
Daniel Fischer
daniel.is.fischer at web.de
Sat Mar 5 17:12:23 EST 2005
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
More information about the Haskell-Cafe
mailing list