Re: Optimizing "counting" GADTs

I meant reflection in the sense of the reflection package. Sorry for the confusion. On Jun 19, 2016 4:28 AM, "Ben Gamari" wrote:

"Edward Z. Yang" writes:

snip

...

...

Dictionaries are harder to come by, but reflection might be an option.

If I understand correctly, even if you have a Typeable dictionary you don't necessarily have a way of constructing the other dictionaries that are available at that type. Maybe that is something worth fixing.

Right; a Typeable dictionary gives you nothing more than the identity of the type. You cannot get any further dictionaries from it. Honestly fixing this seems quite non-trivial (essentially requiring that you construct a symbol name for the desired dictionary and do a symbol table lookup to find it, hoping that the linker didn't decide to drop it due to being unused).

Moreover, it seems possible that providing this ability may have consequences on parametricity. Reflection already comes dangerously close to compromising this property; we are saved only by the fact that a Typeable constraint is needed to request a representation. I'd imagine that allowing the user to produce arbitrary dictionaries from a representation may pose similar issues.

Cheers,

- Ben