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

Dominique Devriese dominique.devriese at cs.kuleuven.be
Sun Sep 19 13:57:25 EDT 2010


Sebastian,

See remarks below.

2010/9/19 Sebastian Menge <sebastian.menge at uni-dortmund.de>:
> 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 ;)

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


More information about the Generics mailing list