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