如何（不安全地）将地图反映为约束？

Question

我想要一个类型类来表示 reified Data.Map.Map 中的成员身份。所以像：

class Reifies s (Map Text v) => IsMember (x :: Symbol) s where
  value :: Proxy s -> Proxy x -> v

然后我想实现一个函数，只要存在符号，它就会返回此类的 Dict 实例：

checkMember :: forall s x v. (KnownSymbol x, Reifies s (Map Text v))
  => proxy x -> Maybe (Dict (IsMember x s))
checkMember sx =
  let m = reflect (Proxy @s)
  in  (_ :: v -> Dict (IsMember x s)) <$> Map.lookup (symbolVal sx) m

我不介意使用unsafeCoerce 来实现checkMember，但即便如此，我仍然无法弄清楚如何执行此操作（填写类型漏洞）。

---

大概的序言：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Constraint(Dict(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Proxy (Proxy(..))
import Data.Reflection (Reifies, reflect)
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)

Answer 1

为什么它必须是一个类IsMember？简单类型怎么样：

newtype Member x s v = Member v

checkMember :: ... => proxy x -> Maybe (Member x s v)

保留Member 抽象允许保留Member x s v 类型的值属于与s 关联的字典的不变量。不需要unsafeCoerce。

从那里，可能还有一些方法可以使用反射将Member 提升回类型级别，但这听起来过于工程化。

---

编辑： 从讨论中可以看出，需求是外部的，没有什么可做的。这是实现checkMember的一种方法。

（reflection 也像这样实现自己的机器。）

我们可以滥用这样一个事实，即 GHC 将具有单个方法且没有超类 class C a where m :: v 的类直接脱糖到未包装的方法 m :: v，并将约束值 C a => b 脱糖到函数 v -> b。

• 我们需要一个没有超类的 IsMember 版本 (IsMember0)
• 我们将IsMember0 x s v => r 包装在一个新类型中，这样它就可以强制转换为IsMember0 x s v -> r (UnsafeMember)

---

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Constraint(Dict(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Proxy (Proxy(..))
import Data.Reflection (Reifies, reflect, reify)
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import Unsafe.Coerce (unsafeCoerce)

type Text = String

class IsMember0 (x :: Symbol) s v | s -> v where
  value0 :: Proxy s -> Proxy x -> v

class (Reifies s (Map Text v), IsMember0 x s v) => IsMember (x :: Symbol) s v | s -> v
instance (Reifies s (Map Text v), IsMember0 x s v) => IsMember (x :: Symbol) s v

value :: IsMember x s v => Proxy s -> Proxy x -> v
value = value0

newtype UnsafeMember x s v = UnsafeMember (IsMember0 x s v => Dict (IsMember x s v))

unsafeMember :: forall x s v. Reifies s (Map Text v) => v -> Dict (IsMember x s v)
unsafeMember v = unsafeCoerce (UnsafeMember @x @s @v Dict) (\ _ _ -> v)

checkMember :: forall s x v proxys proxyx. (KnownSymbol x, Reifies s (Map Text v))
  => proxys s -> proxyx x -> Maybe (Dict (IsMember x s v))
checkMember _ sx =
  let m = reflect (Proxy @s)
  in  unsafeMember <$> Map.lookup (symbolVal sx) m

-- Executable example
main :: IO ()
main = do
  let d = Map.fromList [("foo", 33 :: Int)]
      foo = Proxy :: Proxy "foo"
  reify d (\p ->
    case checkMember p foo of
      Nothing -> fail "Not found"
      Just Dict -> print (value0 p foo))