La riflessione rischia di incoerenza?

Question

Il pacchetto reflection offre una classe

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

e una funzione

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

dato solo questi, si potrebbe fare pasticci piuttosto male dando, per esempio, l'istanza

instance Reifies s Int where 
    reflect _ = 0 

Questo sarebbe male perché, per esempio,

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

potrebbe legittimamente produrre sia 1 (attraverso il normale processo di riflessione) o 0 (specializzandosi la funzione passata prima di applicare reify).

In realtà, questa particolare impresa sembra essere bloccata dall'inclusione di alcune istanze Reifies in Data.Reflection. L'esempio malvagio che ho descritto sarà respinto come sovrapposizione. Se le istanze che si sovrappongono sono abilitate, credo che la specializzazione possa essere bloccata dall'incertezza che la sovrapposizione porta.

Ancora, mi chiedo se c'è qualche modo per esporre questo con un'istanza ombroso, forse con l'aiuto di GADTs o qualcosa del genere.

Answer 1

ho provvisoriamente dicono che non rischia l'incoerenza. Dopo alcuni ritocchi, il modo migliore che poteva venire con dirottare reflect utilizzato INCOHERENT, che è ovviamente sufficiente a produrre l'incoerenza:

{-# LANGUAGE 
    TypeFamilies, FlexibleInstances, MultiParamTypeClasses, 
    ScopedTypeVariables #-} 

import Data.Constraint 
import Data.Proxy 
import Data.Reflection 

instance {-# INCOHERENT #-} Reifies (s :: *) Int where 
    reflect _ = 0 

reflectThis :: forall (s :: *). Dict (Reifies s Int) 
reflectThis = Dict 

-- prints 0 
main = print $ 
    reify (1 :: Int) $ \(p :: Proxy s) -> 
    case reflectThis :: Dict (Reifies s Int) of 
    Dict -> reflect p