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

[Daniel Fischer]

Am Dienstag, 8. März 2005 17:31 schrieben Sie:
> Daniel Fischer wrote:
> >The problem is that for the recursion combinators we need polymorphic
> >recursion functions.
> >For fact3 we need
> >rec2 :: forall l. (HCons a (HCons a l) -> HCons a l),
>
> I dont see why this is illegal... what do we want? take the top two
> items from the stack?

It's illegal, because a type variable may not be instantiated by a 
forall-type; section 7.4.9 of the user's guide:
There is one place you cannot put a forall: you cannot instantiate a type 
variable with a forall-type. So you cannot make a forall-type the argument of 
a type constructor. So these types are illegal: 

   x1 :: [forall a. a->a]
    x2 :: (forall a. a->a, Int)
    x3 :: Maybe (forall a. a->a).

I'd say that also applys to HList,
HCons (forall l. (HCons a (HCons a l) -> HCons a l)) blah
won't work (and my ghci doesn't swallow it).
>
> Take the to N elements from the stack:
>
> class Take l n h t | l n -> h t where
>     take :: l -> n -> (h,t)
> instance Take l HZero HNil l where
>     take l _ = (HNil,l)
> instance Take t n (h',t') => Take (HCons h t) (HSucc n) (HCons h h',t')
> where
>     take (HCons h t) (_::HSucc n) = (HCons h h',t')
>        where (h',t') = take t (undefined::n)
>
Good, but cumbersome. And I'm not sure what the type signature should be for

genrec (HCons rec2 (HCons rec1 (HCons t (HCons b stack))))
    | hHead (b stack) = t stack
    | otherwise = rec2 (HCons (genrec.quote rec2.quote rec1.quote t.quote b)
                                                                 (rec1 stack))

I dare say it would be easier in Haskell-style:

genrec rec2 rec1 t b stack.

> >For the general recursion combinator it's even worse, because
> >rec2 may take n2 elements of certain types from the stack, does something
> > with them and put k2 elements of certain types determined by the types of
> > the consumed elements on the stack, leaving the remainder of the stack
> > unchanged, rec1 takes n1 elements etc. And the numbers n2, n1 . . . and
> > the types depend on the supplied recursion functions.
> >So (reverting to nested pairs notation), we would have to make linrec to
> >accept arguments for rec2 of the types
> >(a,b) -> (r,b),
> >(a,(a1,b)) -> (r,(r1,(r2,b))),
> >(a,(a1,b)) -> (r,b)
> >(a,(a1,(a2,b))) -> (r,b)
> >
> >and so on, for arbitrary munch- and return-numbers, where we don't care
> > what b is. These can't be unified however, so I think it's impossible to
> > transfer these combinators faithfully to a strongly typed language.
> > [Dynamic] won't work either, I believe, because Dynamic objects must be
> > monomorphic, as I've just read in the doc.
> >
> >The point is, in Joy all these functions would have type Stack -> Stack
> > and we can't make a stack of four elements the same type as a stack of
> > six elements using either nested pairs or HLists (correct me if I'm
> > wrong, you know HList better than I do).
>
> They are not the same type, but that are the same Kind, or Type-Familly...

Aye, but as I understand it, once we push the recursion functions on the 
stack, they must be monomorphic, which means, the scheme won't work in 
general. 
>
> class Stack s
> instance Stack HNil
> instance Stack s => Stack (HCons a s)

Isn't this exactly the HList class?
>
> isItAStack :: Stack s => s -> s
> isItAStack = id
>
> >However, Joy has only very few datatypes (according to the introduction I
> >looked at), so
> >
> >data Elem = Bool Bool
> >
> >                 | Char Char
> >                 | Int Integer
> >                 | Double Double
> >                 | String String
> >                 | Fun (Stack -> Stack)
> >                 | List [Elem]
> >                 | Set [Int]
> >
> >type Stack = [Elem]
> >
> >type Joy = State Stack (IO ())
> >
> >looks implementable, probably a lot to write, but not too difficult -
> > maybe, I'll try.
>
> The above can be translated to HLists, the difference is that with
> HLists the types (classes)
> are extensible.

Might well be, only I don't see how (would have to take a lonnnnnnnng look at 
HList, probably).
Of course, doing it the primitive way means a lot of work every time you add a 
new datatype :-(
But for these types, I did it (with a few modifications) and all works fine.
>
> There appears to be no IO in the example Joy code so existentials are
> unneccessary.

No IO around, I only thought I might wish to write an interactive frontend, 
printing out the top of the stack (might be an error message) after each 
step. I haven't got round to that yet, and I don't know whether I will, but I 
think if I do, I'd better use type Joy = IO (State Stack Elem).
>
>     Keean.

Daniel