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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe