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

[Dominique Devriese]

2010/9/20 Sebastian Menge <sebastian.menge at uni-dortmund.de>:
> Am Sun, 19 Sep 2010 19:57:25 +0200
> schrieb Dominique Devriese <dominique.devriese at cs.kuleuven.be>:
>
>> > 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