反思是否存在不连贯性？

Question

该reflection软件包提供了一个类

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

和一个功能

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

只有这些,例如,通过给出实例,可能会使事情变得非常糟糕

instance Reifies s Int where
  reflect _ = 0

这可能很糟糕,例如,

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

可以合法地生成1(通过通常的反射过程)或0(通过在应用之前专门化传递的函数reify).

实际上,这个特定的漏洞似乎被包含在中的一些Reifies实例所阻止Data.Reflection.我描述的邪恶实例将被重复拒绝.如果启用了重叠实例,我相信重复带来的不确定性可能会阻碍专业化.

不过,我想知道是否有一些方法可以在一个阴暗的实例中暴露这个,也许是在GADT或其他类似的帮助下.

Answer 1

我姑且说这不会带来语无伦次的风险。经过一番修改后，我想出了劫持reflect使用的最佳方法INCOHERENT，这毫不奇怪地足以产生不连贯的效果：

{-# 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