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

[Daniel Fischer]

Keean Schupke wrote:
> Daniel Fischer wrote:
> >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 possible, but that seems to have it's own
> > problems).
>
> Well it depends on what you want to do... If the types of elements are
> determined by the computation then you can use an HList as is, and there
> is no problem.

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),
which is illegal in an HList (at least, I haven't found a way to make it 
acceptable) and in tuples.
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).

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 only time there is a problem is if the _type_ of an element to be put
> in an HList depends on an IO action. In this case you need to existentially
> quantify the HList.

How would I do that?
What the user's guide says about existential quantification isn't enough for 
me.
>
> So you can use the HList in both cases, but you have to deal with
> existential
> types if the type of the HList is dependant on IO (you dont have to do this
> if only the value of an element depends on IO).
>
>     Keean.

If you can faithfully implement Greg's code (including fact3-5) using HList, 
I'd be interested to see it, I think HList suits other purposes far better.

Daniel