Greg Buchholz wrote:
Keean Schupke wrote:
I dont see why this is illegal... what do we want? take the top two items from the stack?
With the code below (direct translation from tuples to HLists) I still get an occurs check error when trying to define fact5...
Okay the reason is that types in the code end up depending on values. The
type of the stack changes when items are pushed or popped. So the type of the stack returned from recursive functions depends on the recursion count...
Haskell is not dependantly typed, so cannot deal with types that "depend" on values. This is why your code with tuples, and the HList code (which is really doing the same thing through a defined API) both fall down on the recursion.
One solution is to make all elements the same type and use lists... like:
data Elem = ElemInt Int | ElemChar Char...
But this looses any static type checking. The alternative is to lift the "values"
to the type level, using something like Peano numbers to represent naturals:
data HZero = HZero data HSucc x = HSucc x
Now different values have explictly different types, so we can have types which depend on them...
Attached is an example implementation of "times" using this technique and the
HList library (its not debugged... so there might be some mistakes).
Keean.
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-overlapping-instances #-}
{-# OPTIONS -fallow-undecidable-instances #-}module Joy where import MainGhcGeneric1 data Lit a = Lit a instance Apply (Lit a) s (HCons a s) where apply (Lit a) s = HCons a s data If = If instance Apply t s s' => Apply If (HCons f (HCons t (HCons HTrue s))) s' where apply _ (HCons _ (HCons t (HCons _ s))) = apply t s instance Apply f s s' => Apply If (HCons f (HCons t (HCons HFalse s))) s' where apply _ (HCons f (HCons _ (HCons _ s))) = apply f s data Eq = Eq instance TypeEq a b t => Apply Eq (HCons a (HCons b s)) (HCons t s) where apply _ (HCons a (HCons b s)) = HCons (typeEq a b) s data Dip = Dip instance Apply a s s' => Apply Dip (HCons a (HCons b s)) (HCons b s') where apply _ (HCons a (HCons b s)) = HCons b (apply a s) data Dup = Dup instance Apply Dup (HCons a s) (HCons a (HCons a s)) where apply _ s@(HCons a _) = HCons a s data Pop = Pop instance Apply Pop (HCons a s) s where apply _ (HCons _ s) = s data Swap = Swap instance Apply Swap (HCons a (HCons b s)) (HCons b (HCons a s)) where apply _ (HCons a (HCons b s)) = HCons b (HCons a s) class (HNat a,HNat b) => HAdd a b c | a -> b -> c where hadd :: a -> b -> c instance HAdd HZero HZero HZero where hadd _ _ = hZero instance HAdd HZero (HSucc b) (HSucc b) where hadd _ b = b instance HAdd a b c => HAdd (HSucc a) (HSucc b) (HSucc (HSucc c)) hadd _ _ = hadd (undefined::a) (undefined::b) data Add = Add instance HAdd a b c => Apply Add (HCons a (HCons b s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = HCons (hadd (undefined::a) (undefined::b)) s data Mult = Mult instance HMult a b c => Apply Mult (HCons a (HCons b s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = HCons (hadd (undefined::a) (undefined::b)) s data a @ b = a @ b instance (Apply a s s',Apply b s' s'') => Apply (a @ b) s'' where apply (O a b) s = apply b (apply a s :: s') type Square = Dup @ Mult type Cube = Dup @ Dup @ Mult data I = I instance Apply a s s' => Apply I (HCons a s) s' where apply _ (HCons a s) = apply a s data Times = Times instance Apply Times (HCons p (HCons HZero s)) s where apply _ (HCons _ s) = s instance Apply p s s' => Apply Times (HCons p (HCons (HSucc n) s) (HCons p (HCons n s')) where apply _ (HCons p (HCons _ s)) = HCons p (HCons (undefined::n) (apply p s))
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
