[Hs-Generics] make type witnesses 'phi ix' persistent?

[Sebastian Menge]

Hi

I am playing around with the zipper package. I wrote some helper
functions that allow for a more convenient description of the zipper
state as addresses in the basic form "path at term". The types and
auxiliary functions are given below.

Now I would like to make these addresses "persistent". I want to write
them to disk somehow, and reconstruct them in a later session.

But to reconstruct addresses, I have to create the type witnesses from
the serialization, e.g.:

serialize :: forall phi ix . (Fam phi, El phi ix) 
          => phi ix -> String
serialize MyWitness1 = "MyWitness1"
serialize MyWitness2 = "MyWitness2"

But deserialize wont work:

deserialize :: String -> phi ix -- <--- impossible
deserialize "MyWitness1" = MyWitness1
deserialize "MyWitness2" = MyWitness2

Is there _any_ way to get this going ? Any dirty hacks are also
appreciated ;)

Thanks, Sebastian.

PS here come the relevant types and functions (not tested, just
copy'n'pasted from my sources)


-- more convenient zipper states
data Address phi s t = Address
  { typerep :: phi s
  , value :: s
  , pathrep :: phi t
  , path :: Path
  }

type Path = [Int]

type Nav phi ix= (Loc phi I0 ix -> Maybe (Loc phi I0 ix))

-- convert int-paths to navigations
tonav :: Path -> Nav phi ix
tonav (path) = foldl (>=>) return (map tonav' path) where
  tonav' 0 = down
  tonav' i = tonav' (i-1) >=> right 


-- lookup an address
lookup::(Fam phi, Zipper phi (PF phi), EqS phi) => Address phi s t -> t
lookup a = (pathrep a, path a) @@ (typerep a, value a)


-- explicit lookup on pairs. idea: "path at term"
(@@) :: forall phi ix1 ix2. (Fam phi, Zipper phi (PF phi), EqS phi) 
     => (phi ix2,Path) -> (phi ix1,ix1) -> ix2
(@@) (q,path) (p,e) = case (tonav path $ enter p e) of
  (Just l :: (Maybe (Loc phi I0 ix1))) -> focus q l
  Nothing -> error "invalid path"

-- helper that extracts the focus
focus :: forall phi ix xi. (EqS phi) 
      => phi ix -> (Loc phi I0 xi) -> ix
focus p (Loc q (I0 x) cs) = 
  case eqS p q of
    Just Refl -> x
    _   -> error "focus: types dont match"