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

[Daniel Fischer]

Am Montag, 7. März 2005 17:58 schrieb 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.

One more, you need not supply a type signature for fact, if you provide the 
argument:

fact0 (n,st) = ifte (dup ! pre ! fact ! mult, (pop ! lit 1, (nul, (n,st))))

That's of course rather "unJoyful" :-), but it helps the type-checker (I don't 
know the workings thereof, but it's often the case that functions which don't 
type-check points-free do if sufficiently many arguments are provided).

I don't think that'll help fact3-5, though.

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

I've taken a look, and I must say, I find Haskell more intuitive.

> 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

I think, it would be possible to define recursion combinators for specific 
patterns, like this functions takes 4 elements from the stack, this one 3 and 
so on, but then you would need combinators for all these patterns, which is 
rather cumbersome.

IMO, it's just not the thing to do things in Haskell exactly like in Joy (or 
in Java, prolog, or - horribile dictu- in C/C++). Even if it's possible, the 
spirit of the languages is so different that you should do the same thing in 
different ways. But of course it's interesting to see whether it can be done.

> 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

That's nightmarish enough, because Haskell is strongly typed.
So, if we look at linrec, for example, we find that rec2 and rec1 must return 
the same type as they devour, that's why fact5 doesn't work, because
mult has type 
Num a => (a,(a,b)) -> (a,b).

And, BTW, that's why Keean et al's HList library doesn't help here either, the 
type of an HList determines the number of elements and the type of each, so 
there we face the same problems as with nested tuples. What we need is 
type Stack = [ArbitraryType] (from the HList paper, I surmise that [Dynamic] 
would be possilble, but that seems to have it's own problems).

> 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".

Well, it's fairly amorphous, but it must be the same type in both 
type-expressions, and that's why the points-free definition of fact doesn't 
type-check without the type signature, the 'fact' in the else-branch is used 
at type (Integer,(Integer,a)) and so on, without the type signature, the 
type-checker assumes that it must be instantiated at exactly the same type, 
which it isn't. With the signature, the type-checker knows that 'fact' is 
polymorphic and that it's perfectly all right to instantiate it at a 
different type in the recursive call. 

Well, at least that's what I worked out from my sparse knowledge, if I'm 
wrong, would somebody please correct me?

>
> Thanks,
>
> Greg Buchholz
>
HTH,
Daniel