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@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@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"