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

[Greg Buchholz]

Daniel Fischer wrote:
> Am Freitag, 4. M?rz 2005 19:35 schrieb Greg Buchholz:
> > 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.

   Interesting, I'll have to think it over. (Of course being a relative
newcomer to Haskell, I have to do a lot of thinking when it comes to
most things.)  BTW, can anyone recommend a good introductory resource
for learning about type theory?  I once flipped through Pierce's
Types_and_Programming_Languages, but at first glance, it seemed to be a
little advanced for my understanding (the foreign-looking equations per
word ratio seemed a little too high).

> 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)

    Nice.  Definitely something for me to study.  Of course, IFAICT, the
main motivation for Joy is to try and define everything in terms of
function composition instead of function application.
    
> I don't know Joy, but probably there the stack is (roughly) a heterogenous 
> list, which is hard to model in Haskell,

    Yeah, I don't know Joy either, other than reading a few documents,
but I do think its stack is really heterogenous list.  The one reason I
was thinking this might be doable in Haskell, is the fact that the few
combinators I looked at don't recurse down the whole "stack".  That, of
course, would be a complete nightmare in Haskell.   Instead they take a
"stack", munge a few (finite number of) items at the top, and return
another "stack".  I was hoping that the type variable "a" in (Integer,
a) -> (Integer, a) would be amorphous enough to match whatever was left
over after grabbing a few items off the top of this "stack".

Thanks,

Greg Buchholz