Как (небезопасно) отразить карту в качестве ограничения? - PullRequest
Новая
       30

Как (небезопасно) отразить карту в качестве ограничения?

0 голосов
/ 18 декабря 2018

Мне нужен класс типов, представляющий членство в 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)

1 Ответ

0 голосов
/ 18 декабря 2018

Почему это должен быть класс IsMember?Как насчет простого типа: 

newtype Member x s v = Member v

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

Сохранение Member abstract позволяет сохранить инвариант, что значение типа 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))
...