
Sebastian,
See remarks below.
2010/9/19 Sebastian Menge
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 ;)
I didn't test this, but maybe it helps to dualize the deserialize function: deserialize :: String -> (forall ix. phi ix -> r) -> r deserialize "MyWitness1" f = f MyWitness1 deserialize "MyWitness2" f = f MyWitness2 I expect there's no way to do this with a function f whose return type depends on the type ix. cheers Dominique