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

2010/9/20 Sebastian Menge :

Am Sun, 19 Sep 2010 19:57:25 +0200 schrieb Dominique Devriese :

...

...

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.

Why not? I guess, there is a good formal reason for this?

Informally: because then the deserialize function's type depends on the particular String it receives, which seems to require a dependently typed language (like Agda where this is not difficult). Formally: not sure if a formal argument can be given for this. Dominique