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

[Keean Schupke]

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?

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)

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

class Stack s
instance Stack HNil
instance Stack s => Stack (HCons a s)

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.

There appears to be no IO in the example Joy code so existentials are 
unneccessary.

    Keean.