dimanche 10 janvier 2016

Does reflection risk incoherence?

The reflection package offers a class

class Reifies s a | s -> a where
  reflect :: proxy s -> a

and a function

reify :: a -> (forall s . Reifies s a => Proxy s -> r) -> r

Given only these, one could mess things up rather badly by giving, for example, the instance

instance Reifies s Int where
  reflect _ = 0

This would be bad because, for instance,

reify (1 :: Int) $ \p -> reflect p

could legitimately produce either 1 (via the usual reflection process) or 0 (by specializing the passed function before applying reify).

In reality, this particular exploit seems to be blocked by the inclusion of a few Reifies instances in Data.Reflection. The evil instance I described will be rejected as overlapping. If overlapping instances are enabled, I believe the specialization may be blocked by the uncertainty overlapping brings.

Still, I'm wondering if there's some way to expose this with a shady instance, perhaps with the help of GADTs or some such.





Aucun commentaire:

Enregistrer un commentaire