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

[Greg Buchholz]

Daniel Fischer wrote:
> 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.

    Hmm.  The standard Joy combinators probably can't be typed, so maybe
my next step would be to find/create a recursion combinator with a
static type.  Surely one must exist? If you can have a typed lambda
calculus, you must be able to have a typed SK combinator calculus,
right? (Now I'm way out of my league.)  I'll have to think some more on
why you couldn't have a recursion combinator which was more generic than
the one that takes 3 items off the stack, or 4 items, rather than n
items.  Or maybe the whole idea of using a "stack" is the essential
weakness.

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

    Yeah.  I'm only in it for the brain exercise, not to convert the
masses over to Joy ;-)

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

    That pretty much sums up why I thought the whole crazy scheme might
work, only in better words.


Greg Buchholz