module FoldRep
where

type Id a = a



data EPT a b = EP{to :: a -> b, from :: b -> a}
refl :: EPT a a
refl = EP id id

newtype Forall f = Forall { fromForall :: forall b . f b}

data Rep f a = RInt (EPT (f a) Int)
		 | RVar (EPT (f a) a)
		 | RBVar
		 | forall g h . RProd (Rep g a) (Rep h a) 
				(EPT (f a) (g a,h a))
		 | forall g h . RSum (Rep g a) (Rep h a) 
				(EPT (f a) (Either (g a) (h a)))
		 | forall g h . RArrow (Rep g a) (Rep h a) 
				(EPT (f a) (g a -> h a))


app' :: forall f a . (Rep f a) -> (a -> ()) -> (f a -> ())
app' (RInt ep) f x = ()
app' (RVar ep) (f::(a -> ())) (x::(f a)) = f (to ep x)
app' RBVar f x = ()
app' (RProd rB rC ep) f x = 
  let (x1 ,x2) = to ep x in
  let () = app' rB f x1 in
  app' rC f x2
app' (RSum rB rC ep) f x = 
  case (to ep x) of
    Left x1 -> app' rB f x1;
    Right x2 -> app' rC f x2
app' (RArrow rB rC ep) f x = () -- app' doesn't go under functions

fold' :: forall f a b . (Rep f a) -> (b -> a -> b) -> (b -> f a -> b)
fold' (RInt ep) f v x = v
fold' (RVar ep) f v x = f v (to ep x)
fold' RBVar f v x = v
fold' (RProd rB rC ep) f v x = 
  let (x1 ,x2) = to ep x in
  let v' = fold' rB f v x1 in
  fold' rC f v' x2
fold' (RSum rB rC ep) f v x = 
  case (to ep x) of
    Left x1 -> fold' rB f v x1;
    Right x2 -> fold' rC f v x2
fold' (RArrow rB rC ep) f v x = v -- ignore function pointers...



-- Idea: Add enough stuff to this that you can go "map' rList" and get list
-- map, etc.
-- Also, consider adding symbol tables to some cases of Rep and allowing
-- generic functions to look up overriding definitions of themselves.
-- So, if you want to have lists print out bracketed, you would 
-- replace the plain RCon "[]" constructor with an ROverride constructor
-- that contains a dictionary of string, Dynamic pairs.  Then rShow
-- would have a case for ROverride that looks up the name "rShow" in
-- the provided symbol table, and dynamically casts the result to 
-- the required type.  If the cast fails, then rShow could either stop with
-- an error or continue by falling through to the non-overrided 
-- definition (override could have a Bool flag that has a hint for this)
-- Note that it is up to rShow to handle the overriding behavior correctly and
-- up to the type representation's provider to provide a good 
-- implementation of rShow.
-- Does this give us open recursion?  That is, can we combine overridings that 
-- don't know about each other dynamically?  Similarly, does this give us
-- extensible sums for free?  

-- I think it does!  In fact the types of the extensible sums/dictionaries 
-- needn't even be 
-- uniform or unique (the symbol table could have multiple entries).

-- Cool!